Theorem dfsn2 4605

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 4595	. 2 ⊢ {𝐴, 𝐴} = ({𝐴} ∪ {𝐴})
2		unidm 4123	. 2 ⊢ ({𝐴} ∪ {𝐴}) = {𝐴}
3	1, 2	eqtr2i 2754	1 ⊢ {𝐴} = {𝐴, 𝐴}

Syntax hints:   = wceq 1540   ∪ cun 3915  {csn 4592  {cpr 4594

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3922  df-pr 4595

This theorem is referenced by:  nfsn  4674  disjprsn  4681  tpidm12  4722  tpidm  4725  ifpprsnss  4731  preqsnd  4826  elpreqprlem  4833  opidg  4859  unisng  4892  intsng  4950  vsnex  5392  opeqsng  5466  propeqop  5470  relop  5817  funopg  6553  f1oprswap  6847  fnprb  7185  enpr1g  8997  prfi  9281  supsn  9431  infsn  9465  pr2ne  9964  prdom2  9966  wuntp  10671  wunsn  10676  grusn  10764  prunioo  13449  hashprg  14367  hashfun  14409  hashle2pr  14449  lcmfsn  16612  lubsn  18448  indislem  22894  hmphindis  23691  wilthlem2  26986  negs1s  27940  upgrex  29026  umgrnloop0  29043  edglnl  29077  usgrnloop0ALT  29139  uspgr1v1eop  29183  1loopgruspgr  29435  1egrvtxdg0  29446  umgr2v2eedg  29459  umgr2v2e  29460  ifpsnprss  29558  upgriswlk  29576  clwwlkn1  29977  upgr1wlkdlem1  30081  1to2vfriswmgr  30215  esumpr2  34064  dvh2dim  41446  wopprc  43026  clsk1indlem4  44040  sge0prle  46406  meadjun  46467  elsprel  47480  sclnbgrelself  47852  upgrwlkupwlk  48132