Theorem dfsn2 4580

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

Syntax hints:   = wceq 1542   ∪ cun 3887  {csn 4567  {cpr 4569

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894  df-pr 4570

This theorem is referenced by:  nfsn  4651  disjprsn  4658  tpidm12  4699  tpidm  4702  ifpprsnss  4708  preqsnd  4802  elpreqprlem  4809  opidg  4835  unisng  4868  intsng  4925  vsnex  5377  snex  5381  opeqsng  5457  propeqop  5461  relop  5805  funopg  6532  f1oprswap  6825  fnprb  7163  enpr1g  8970  prfi  9234  supsn  9386  infsn  9420  pr2ne  9927  prdom2  9928  wuntp  10634  wunsn  10639  grusn  10727  prunioo  13434  hashprg  14357  hashfun  14399  hashle2pr  14439  lcmfsn  16604  lubsn  18448  indislem  22965  hmphindis  23762  wilthlem2  27032  neg1s  28019  upgrex  29161  umgrnloop0  29178  edglnl  29212  usgrnloop0ALT  29274  uspgr1v1eop  29318  1loopgruspgr  29569  1egrvtxdg0  29580  umgr2v2eedg  29593  umgr2v2e  29594  ifpsnprss  29691  upgriswlk  29709  clwwlkn1  30111  upgr1wlkdlem1  30215  1to2vfriswmgr  30349  esumpr2  34211  dvh2dim  41891  wopprc  43458  clsk1indlem4  44471  sge0prle  46829  meadjun  46890  elsprel  47935  sclnbgrelself  48324  upgrwlkupwlk  48616