Theorem dfsn2 4591

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 4581	. 2 ⊢ {𝐴, 𝐴} = ({𝐴} ∪ {𝐴})
2		unidm 4107	. 2 ⊢ ({𝐴} ∪ {𝐴}) = {𝐴}
3	1, 2	eqtr2i 2758	1 ⊢ {𝐴} = {𝐴, 𝐴}

Syntax hints:   = wceq 1541   ∪ cun 3897  {csn 4578  {cpr 4580

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-un 3904  df-pr 4581

This theorem is referenced by:  nfsn  4662  disjprsn  4669  tpidm12  4710  tpidm  4713  ifpprsnss  4719  preqsnd  4813  elpreqprlem  4820  opidg  4846  unisng  4879  intsng  4936  vsnex  5377  opeqsng  5449  propeqop  5453  relop  5797  funopg  6524  f1oprswap  6817  fnprb  7152  enpr1g  8958  prfi  9222  supsn  9374  infsn  9408  pr2ne  9913  prdom2  9914  wuntp  10620  wunsn  10625  grusn  10713  prunioo  13395  hashprg  14316  hashfun  14358  hashle2pr  14398  lcmfsn  16560  lubsn  18403  indislem  22942  hmphindis  23739  wilthlem2  27033  negs1s  27996  upgrex  29114  umgrnloop0  29131  edglnl  29165  usgrnloop0ALT  29227  uspgr1v1eop  29271  1loopgruspgr  29523  1egrvtxdg0  29534  umgr2v2eedg  29547  umgr2v2e  29548  ifpsnprss  29645  upgriswlk  29663  clwwlkn1  30065  upgr1wlkdlem1  30169  1to2vfriswmgr  30303  esumpr2  34173  dvh2dim  41644  wopprc  43214  clsk1indlem4  44227  sge0prle  46587  meadjun  46648  elsprel  47663  sclnbgrelself  48036  upgrwlkupwlk  48328