Theorem dfsn2 4590

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

Syntax hints:   = wceq 1540   ∪ cun 3901  {csn 4577  {cpr 4579

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 3438  df-un 3908  df-pr 4580

This theorem is referenced by:  nfsn  4659  disjprsn  4666  tpidm12  4707  tpidm  4710  ifpprsnss  4716  preqsnd  4810  elpreqprlem  4817  opidg  4843  unisng  4876  intsng  4933  vsnex  5373  opeqsng  5446  propeqop  5450  relop  5793  funopg  6516  f1oprswap  6808  fnprb  7144  enpr1g  8948  prfi  9213  supsn  9363  infsn  9397  pr2ne  9899  prdom2  9900  wuntp  10605  wunsn  10610  grusn  10698  prunioo  13384  hashprg  14302  hashfun  14344  hashle2pr  14384  lcmfsn  16546  lubsn  18388  indislem  22885  hmphindis  23682  wilthlem2  26977  negs1s  27938  upgrex  29037  umgrnloop0  29054  edglnl  29088  usgrnloop0ALT  29150  uspgr1v1eop  29194  1loopgruspgr  29446  1egrvtxdg0  29457  umgr2v2eedg  29470  umgr2v2e  29471  ifpsnprss  29568  upgriswlk  29586  clwwlkn1  29985  upgr1wlkdlem1  30089  1to2vfriswmgr  30223  esumpr2  34034  dvh2dim  41424  wopprc  43003  clsk1indlem4  44017  sge0prle  46382  meadjun  46443  elsprel  47459  sclnbgrelself  47832  upgrwlkupwlk  48124