Theorem dfsn2 4571

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 4561	. 2 ⊢ {𝐴, 𝐴} = ({𝐴} ∪ {𝐴})
2		unidm 4082	. 2 ⊢ ({𝐴} ∪ {𝐴}) = {𝐴}
3	1, 2	eqtr2i 2767	1 ⊢ {𝐴} = {𝐴, 𝐴}

Syntax hints:   = wceq 1539   ∪ cun 3881  {csn 4558  {cpr 4560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-un 3888  df-pr 4561

This theorem is referenced by:  nfsn  4640  disjprsn  4647  tpidm12  4688  tpidm  4691  ifpprsnss  4697  preqsnd  4786  elpreqprlem  4793  opidg  4820  unisng  4857  intsng  4913  snex  5349  opeqsng  5411  propeqop  5415  relop  5748  funopg  6452  f1oprswap  6743  fnprb  7066  enpr1g  8764  supsn  9161  infsn  9194  prdom2  9693  wuntp  10398  wunsn  10403  grusn  10491  prunioo  13142  hashprg  14038  hashfun  14080  hashle2pr  14119  lcmfsn  16268  lubsn  18115  indislem  22058  hmphindis  22856  wilthlem2  26123  upgrex  27365  umgrnloop0  27382  edglnl  27416  usgrnloop0ALT  27475  uspgr1v1eop  27519  1loopgruspgr  27770  1egrvtxdg0  27781  umgr2v2eedg  27794  umgr2v2e  27795  ifpsnprss  27892  upgriswlk  27910  clwwlkn1  28306  upgr1wlkdlem1  28410  1to2vfriswmgr  28544  esumpr2  31935  dvh2dim  39386  wopprc  40768  clsk1indlem4  41543  sge0prle  43829  meadjun  43890  elsprel  44815  upgrwlkupwlk  45190