Theorem dfsn2 4593

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 4583	. 2 ⊢ {𝐴, 𝐴} = ({𝐴} ∪ {𝐴})
2		unidm 4109	. 2 ⊢ ({𝐴} ∪ {𝐴}) = {𝐴}
3	1, 2	eqtr2i 2760	1 ⊢ {𝐴} = {𝐴, 𝐴}

Syntax hints:   = wceq 1541   ∪ cun 3899  {csn 4580  {cpr 4582

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-pr 4583

This theorem is referenced by:  nfsn  4664  disjprsn  4671  tpidm12  4712  tpidm  4715  ifpprsnss  4721  preqsnd  4815  elpreqprlem  4822  opidg  4848  unisng  4881  intsng  4938  vsnex  5379  opeqsng  5451  propeqop  5455  relop  5799  funopg  6526  f1oprswap  6819  fnprb  7154  enpr1g  8960  prfi  9224  supsn  9376  infsn  9410  pr2ne  9915  prdom2  9916  wuntp  10622  wunsn  10627  grusn  10715  prunioo  13397  hashprg  14318  hashfun  14360  hashle2pr  14400  lcmfsn  16562  lubsn  18405  indislem  22944  hmphindis  23741  wilthlem2  27035  neg1s  28023  upgrex  29165  umgrnloop0  29182  edglnl  29216  usgrnloop0ALT  29278  uspgr1v1eop  29322  1loopgruspgr  29574  1egrvtxdg0  29585  umgr2v2eedg  29598  umgr2v2e  29599  ifpsnprss  29696  upgriswlk  29714  clwwlkn1  30116  upgr1wlkdlem1  30220  1to2vfriswmgr  30354  esumpr2  34224  dvh2dim  41705  wopprc  43272  clsk1indlem4  44285  sge0prle  46645  meadjun  46706  elsprel  47721  sclnbgrelself  48094  upgrwlkupwlk  48386