Theorem dfsn2 4597

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 4591	. 2 ⊢ {𝐴, 𝐴} = ({𝐴} ∪ {𝐴})
2		unidm 4159	. 2 ⊢ ({𝐴} ∪ {𝐴}) = {𝐴}
3	1, 2	eqtr2i 2787	1 ⊢ {𝐴} = {𝐴, 𝐴}

This proof depends on syntax axioms:   = wceq 1570   ∪ cun 4152  {csn 4588  {cpr 4590

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-un 4154  df-pr 4591

This theorem is used by:  nfsn  4669  disjprsn  4676  tpidm12  4718  tpidm  4721  ifpprsnss  4727  preqsnd  4819  elpreqprlem  4826  opidg  4857  unisng  4890  intsng  4948  vsnex  5400  snex  5404  opeqsng  5482  propeqop  5486  relop  5838  funopg  6602  f1oprswap  6901  fnprb  7245  enpr1g  9088  prfi  9353  supsn  9502  infsn  9536  pr2ne  10123  prdom2  10124  wuntp  10835  wunsn  10840  grusn  10928  prunioo  13652  hashprg  14580  hashfun  14623  hashle2pr  14663  lcmfsn  16854  lubsn  18706  indislem  23373  hmphindis  24171  wilthlem2  27453  neg1s  28470  upgrex  29727  umgrnloop0  29744  edglnl  29778  usgrnloop0ALT  29843  uspgr1v1eop  29887  1loopgruspgr  30138  1egrvtxdg0  30149  umgr2v2eedg  30162  umgr2v2e  30163  ifpsnprss  30260  upgriswlk  30278  clwwlkn1  30689  upgr1wlkdlem1  30793  1to2vfriswmgr  30937  esumpr2  34810  dvh2dim  42768  wopprc  44303  clsk1indlem4  45305  sge0prle  47684  meadjun  47745  elsprel  48830  sclnbgrelself  49219  upgrwlkupwlk  49511