Theorem dfsn2 4602

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 4592	. 2 ⊢ {𝐴, 𝐴} = ({𝐴} ∪ {𝐴})
2		unidm 4120	. 2 ⊢ ({𝐴} ∪ {𝐴}) = {𝐴}
3	1, 2	eqtr2i 2753	1 ⊢ {𝐴} = {𝐴, 𝐴}

Syntax hints:   = wceq 1540   ∪ cun 3912  {csn 4589  {cpr 4591

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-un 3919  df-pr 4592

This theorem is referenced by:  nfsn  4671  disjprsn  4678  tpidm12  4719  tpidm  4722  ifpprsnss  4728  preqsnd  4823  elpreqprlem  4830  opidg  4856  unisng  4889  intsng  4947  vsnex  5389  opeqsng  5463  propeqop  5467  relop  5814  funopg  6550  f1oprswap  6844  fnprb  7182  enpr1g  8994  prfi  9274  supsn  9424  infsn  9458  pr2ne  9957  prdom2  9959  wuntp  10664  wunsn  10669  grusn  10757  prunioo  13442  hashprg  14360  hashfun  14402  hashle2pr  14442  lcmfsn  16605  lubsn  18441  indislem  22887  hmphindis  23684  wilthlem2  26979  negs1s  27933  upgrex  29019  umgrnloop0  29036  edglnl  29070  usgrnloop0ALT  29132  uspgr1v1eop  29176  1loopgruspgr  29428  1egrvtxdg0  29439  umgr2v2eedg  29452  umgr2v2e  29453  ifpsnprss  29551  upgriswlk  29569  clwwlkn1  29970  upgr1wlkdlem1  30074  1to2vfriswmgr  30208  esumpr2  34057  dvh2dim  41439  wopprc  43019  clsk1indlem4  44033  sge0prle  46399  meadjun  46460  elsprel  47476  sclnbgrelself  47848  upgrwlkupwlk  48128