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 2784	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 2732

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 2739  df-cleq 2752  df-clel 2835  df-v 3452  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  5400  snex  5404  opeqsng  5480  propeqop  5484  relop  5830  funopg  6567  f1oprswap  6863  fnprb  7207  enpr1g  9029  prfi  9293  supsn  9443  infsn  9477  pr2ne  10008  prdom2  10009  wuntp  10720  wunsn  10725  grusn  10813  prunioo  13534  hashprg  14459  hashfun  14502  hashle2pr  14542  lcmfsn  16725  lubsn  18570  indislem  23225  hmphindis  24023  wilthlem2  27305  neg1s  28292  upgrex  29549  umgrnloop0  29566  edglnl  29600  usgrnloop0ALT  29665  uspgr1v1eop  29709  1loopgruspgr  29960  1egrvtxdg0  29971  umgr2v2eedg  29984  umgr2v2e  29985  ifpsnprss  30082  upgriswlk  30100  clwwlkn1  30511  upgr1wlkdlem1  30615  1to2vfriswmgr  30759  esumpr2  34577  dvh2dim  42318  wopprc  43871  clsk1indlem4  44884  sge0prle  47229  meadjun  47290  elsprel  48375  sclnbgrelself  48764  upgrwlkupwlk  49056