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 4587	. 2 ⊢ {𝐴, 𝐴} = ({𝐴} ∪ {𝐴})
2		unidm 4104	. 2 ⊢ ({𝐴} ∪ {𝐴}) = {𝐴}
3	1, 2	eqtr2i 2785	1 ⊢ {𝐴} = {𝐴, 𝐴}

This proof depends on syntax axioms:   = wceq 1570   ∪ cun 3897  {csn 4584  {cpr 4586

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-pr 4587

This theorem is used by:  nfsn  4668  disjprsn  4675  tpidm12  4716  tpidm  4719  ifpprsnss  4725  preqsnd  4819  elpreqprlem  4826  opidg  4852  unisng  4885  intsng  4943  vsnex  5393  snex  5397  opeqsng  5475  propeqop  5479  relop  5828  funopg  6572  f1oprswap  6868  fnprb  7212  enpr1g  9043  prfi  9308  supsn  9458  infsn  9492  pr2ne  10077  prdom2  10078  wuntp  10789  wunsn  10794  grusn  10882  prunioo  13605  hashprg  14532  hashfun  14575  hashle2pr  14615  lcmfsn  16803  lubsn  18649  indislem  23311  hmphindis  24109  wilthlem2  27389  neg1s  28406  upgrex  29663  umgrnloop0  29680  edglnl  29714  usgrnloop0ALT  29779  uspgr1v1eop  29823  1loopgruspgr  30074  1egrvtxdg0  30085  umgr2v2eedg  30098  umgr2v2e  30099  ifpsnprss  30196  upgriswlk  30214  clwwlkn1  30625  upgr1wlkdlem1  30729  1to2vfriswmgr  30873  esumpr2  34692  dvh2dim  42482  wopprc  44016  clsk1indlem4  45029  sge0prle  47380  meadjun  47441  elsprel  48526  sclnbgrelself  48915  upgrwlkupwlk  49207