Theorem dfsn2 4614

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 4604	. 2 ⊢ {𝐴, 𝐴} = ({𝐴} ∪ {𝐴})
2		unidm 4132	. 2 ⊢ ({𝐴} ∪ {𝐴}) = {𝐴}
3	1, 2	eqtr2i 2759	1 ⊢ {𝐴} = {𝐴, 𝐴}

Syntax hints:   = wceq 1540   ∪ cun 3924  {csn 4601  {cpr 4603

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-un 3931  df-pr 4604

This theorem is referenced by:  nfsn  4683  disjprsn  4690  tpidm12  4731  tpidm  4734  ifpprsnss  4740  preqsnd  4835  elpreqprlem  4842  opidg  4868  unisng  4901  intsng  4959  vsnex  5404  opeqsng  5478  propeqop  5482  relop  5830  funopg  6570  f1oprswap  6862  fnprb  7200  enpr1g  9037  prfi  9335  supsn  9485  infsn  9519  pr2ne  10018  prdom2  10020  wuntp  10725  wunsn  10730  grusn  10818  prunioo  13498  hashprg  14413  hashfun  14455  hashle2pr  14495  lcmfsn  16654  lubsn  18492  indislem  22938  hmphindis  23735  wilthlem2  27031  negs1s  27985  upgrex  29071  umgrnloop0  29088  edglnl  29122  usgrnloop0ALT  29184  uspgr1v1eop  29228  1loopgruspgr  29480  1egrvtxdg0  29491  umgr2v2eedg  29504  umgr2v2e  29505  ifpsnprss  29603  upgriswlk  29621  clwwlkn1  30022  upgr1wlkdlem1  30126  1to2vfriswmgr  30260  esumpr2  34098  dvh2dim  41464  wopprc  43054  clsk1indlem4  44068  sge0prle  46430  meadjun  46491  elsprel  47489  sclnbgrelself  47861  upgrwlkupwlk  48115