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  5372  snex  5376  opeqsng  5451  propeqop  5455  relop  5799  funopg  6526  f1oprswap  6819  fnprb  7156  enpr1g  8963  prfi  9227  supsn  9379  infsn  9413  pr2ne  9918  prdom2  9919  wuntp  10625  wunsn  10630  grusn  10718  prunioo  13425  hashprg  14348  hashfun  14390  hashle2pr  14430  lcmfsn  16595  lubsn  18439  indislem  22975  hmphindis  23772  wilthlem2  27046  neg1s  28033  upgrex  29175  umgrnloop0  29192  edglnl  29226  usgrnloop0ALT  29288  uspgr1v1eop  29332  1loopgruspgr  29584  1egrvtxdg0  29595  umgr2v2eedg  29608  umgr2v2e  29609  ifpsnprss  29706  upgriswlk  29724  clwwlkn1  30126  upgr1wlkdlem1  30230  1to2vfriswmgr  30364  esumpr2  34227  dvh2dim  41905  wopprc  43476  clsk1indlem4  44489  sge0prle  46847  meadjun  46908  elsprel  47947  sclnbgrelself  48336  upgrwlkupwlk  48628