Theorem dfsn2 4581

Description: Alternate definition of singleton. Definition 5.1 of [TakeutiZaring] p. 15. (Contributed by NM, 24-Apr-1994.)

Assertion

Ref	Expression
dfsn2	⊢ {𝐴} = {𝐴, 𝐴}

Proof of Theorem dfsn2

Step	Hyp	Ref	Expression
1		df-pr 4571	. 2 ⊢ {𝐴, 𝐴} = ({𝐴} ∪ {𝐴})
2		unidm 4098	. 2 ⊢ ({𝐴} ∪ {𝐴}) = {𝐴}
3	1, 2	eqtr2i 2761	1 ⊢ {𝐴} = {𝐴, 𝐴}

Syntax hints:   = wceq 1542   ∪ cun 3888  {csn 4568  {cpr 4570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-un 3895  df-pr 4571

This theorem is referenced by:  nfsn  4652  disjprsn  4659  tpidm12  4700  tpidm  4703  ifpprsnss  4709  preqsnd  4803  elpreqprlem  4810  opidg  4836  unisng  4869  intsng  4926  vsnex  5370  snex  5374  opeqsng  5449  propeqop  5453  relop  5797  funopg  6524  f1oprswap  6817  fnprb  7154  enpr1g  8961  prfi  9225  supsn  9377  infsn  9411  pr2ne  9916  prdom2  9917  wuntp  10623  wunsn  10628  grusn  10716  prunioo  13398  hashprg  14319  hashfun  14361  hashle2pr  14401  lcmfsn  16563  lubsn  18406  indislem  22943  hmphindis  23740  wilthlem2  27019  neg1s  28007  upgrex  29149  umgrnloop0  29166  edglnl  29200  usgrnloop0ALT  29262  uspgr1v1eop  29306  1loopgruspgr  29558  1egrvtxdg0  29569  umgr2v2eedg  29582  umgr2v2e  29583  ifpsnprss  29680  upgriswlk  29698  clwwlkn1  30100  upgr1wlkdlem1  30204  1to2vfriswmgr  30338  esumpr2  34217  dvh2dim  41882  wopprc  43461  clsk1indlem4  44474  sge0prle  46833  meadjun  46894  elsprel  47909  sclnbgrelself  48282  upgrwlkupwlk  48574