Theorem dfsn2 4644

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 4634	. 2 ⊢ {𝐴, 𝐴} = ({𝐴} ∪ {𝐴})
2		unidm 4167	. 2 ⊢ ({𝐴} ∪ {𝐴}) = {𝐴}
3	1, 2	eqtr2i 2764	1 ⊢ {𝐴} = {𝐴, 𝐴}

Syntax hints:   = wceq 1537   ∪ cun 3961  {csn 4631  {cpr 4633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-un 3968  df-pr 4634

This theorem is referenced by:  nfsn  4712  disjprsn  4719  tpidm12  4760  tpidm  4763  ifpprsnss  4769  preqsnd  4864  elpreqprlem  4871  opidg  4897  unisng  4930  intsng  4988  vsnex  5440  opeqsng  5513  propeqop  5517  relop  5864  funopg  6602  f1oprswap  6893  fnprb  7228  enpr1g  9062  prfi  9361  supsn  9510  infsn  9543  pr2ne  10042  prdom2  10044  wuntp  10749  wunsn  10754  grusn  10842  prunioo  13518  hashprg  14431  hashfun  14473  hashle2pr  14513  lcmfsn  16669  lubsn  18540  indislem  23023  hmphindis  23821  wilthlem2  27127  negs1s  28074  upgrex  29124  umgrnloop0  29141  edglnl  29175  usgrnloop0ALT  29237  uspgr1v1eop  29281  1loopgruspgr  29533  1egrvtxdg0  29544  umgr2v2eedg  29557  umgr2v2e  29558  ifpsnprss  29656  upgriswlk  29674  clwwlkn1  30070  upgr1wlkdlem1  30174  1to2vfriswmgr  30308  esumpr2  34048  dvh2dim  41428  wopprc  43019  clsk1indlem4  44034  sge0prle  46357  meadjun  46418  elsprel  47400  sclnbgrelself  47772  upgrwlkupwlk  47984