Theorem dfsn2 4633

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

Syntax hints:   = wceq 1533   ∪ cun 3938  {csn 4620  {cpr 4622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-v 3468  df-un 3945  df-pr 4623

This theorem is referenced by:  nfsn  4703  disjprsn  4710  tpidm12  4751  tpidm  4754  ifpprsnss  4760  preqsnd  4851  elpreqprlem  4858  opidg  4884  unisng  4919  intsng  4979  vsnex  5419  opeqsng  5493  propeqop  5497  relop  5840  funopg  6572  f1oprswap  6867  fnprb  7201  enpr1g  9015  supsn  9462  infsn  9495  pr2ne  9994  prdom2  9996  wuntp  10701  wunsn  10706  grusn  10794  prunioo  13454  hashprg  14351  hashfun  14393  hashle2pr  14434  lcmfsn  16568  lubsn  18434  indislem  22813  hmphindis  23611  wilthlem2  26905  upgrex  28776  umgrnloop0  28793  edglnl  28827  usgrnloop0ALT  28886  uspgr1v1eop  28930  1loopgruspgr  29181  1egrvtxdg0  29192  umgr2v2eedg  29205  umgr2v2e  29206  ifpsnprss  29304  upgriswlk  29322  clwwlkn1  29718  upgr1wlkdlem1  29822  1to2vfriswmgr  29956  esumpr2  33520  dvh2dim  40772  wopprc  42224  clsk1indlem4  43250  sge0prle  45568  meadjun  45629  elsprel  46594  upgrwlkupwlk  46969