Theorem dfsn2 4641

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 4631	. 2 ⊢ {𝐴, 𝐴} = ({𝐴} ∪ {𝐴})
2		unidm 4152	. 2 ⊢ ({𝐴} ∪ {𝐴}) = {𝐴}
3	1, 2	eqtr2i 2762	1 ⊢ {𝐴} = {𝐴, 𝐴}

Syntax hints:   = wceq 1542   ∪ cun 3946  {csn 4628  {cpr 4630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3953  df-pr 4631

This theorem is referenced by:  nfsn  4711  disjprsn  4718  tpidm12  4759  tpidm  4762  ifpprsnss  4768  preqsnd  4859  elpreqprlem  4866  opidg  4892  unisng  4929  intsng  4989  vsnex  5429  opeqsng  5503  propeqop  5507  relop  5849  funopg  6580  f1oprswap  6875  fnprb  7207  enpr1g  9017  supsn  9464  infsn  9497  pr2ne  9996  prdom2  9998  wuntp  10703  wunsn  10708  grusn  10796  prunioo  13455  hashprg  14352  hashfun  14394  hashle2pr  14435  lcmfsn  16569  lubsn  18432  indislem  22495  hmphindis  23293  wilthlem2  26563  upgrex  28342  umgrnloop0  28359  edglnl  28393  usgrnloop0ALT  28452  uspgr1v1eop  28496  1loopgruspgr  28747  1egrvtxdg0  28758  umgr2v2eedg  28771  umgr2v2e  28772  ifpsnprss  28870  upgriswlk  28888  clwwlkn1  29284  upgr1wlkdlem1  29388  1to2vfriswmgr  29522  esumpr2  33054  dvh2dim  40305  wopprc  41755  clsk1indlem4  42781  sge0prle  45104  meadjun  45165  elsprel  46130  upgrwlkupwlk  46505