Theorem dfsn2 4568

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 4558	. 2 ⊢ {𝐴, 𝐴} = ({𝐴} ∪ {𝐴})
2		unidm 4087	. 2 ⊢ ({𝐴} ∪ {𝐴}) = {𝐴}
3	1, 2	eqtr2i 2763	1 ⊢ {𝐴} = {𝐴, 𝐴}

Syntax hints:   = wceq 1547   ∪ cun 3881  {csn 4555  {cpr 4557

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-un 3888  df-pr 4558

This theorem is referenced by:  nfsn  4639  disjprsn  4646  tpidm12  4687  tpidm  4690  ifpprsnss  4696  preqsnd  4790  elpreqprlem  4797  opidg  4823  unisng  4856  intsng  4913  vsnex  5364  snex  5368  opeqsng  5444  propeqop  5448  relop  5792  funopg  6519  f1oprswap  6812  fnprb  7152  enpr1g  8960  prfi  9224  supsn  9376  infsn  9410  pr2ne  9918  prdom2  9919  wuntp  10625  wunsn  10630  grusn  10718  prunioo  13425  hashprg  14348  hashfun  14390  hashle2pr  14430  lcmfsn  16595  lubsn  18439  indislem  22983  hmphindis  23780  wilthlem2  27050  neg1s  28037  upgrex  29179  umgrnloop0  29196  edglnl  29230  usgrnloop0ALT  29292  uspgr1v1eop  29336  1loopgruspgr  29587  1egrvtxdg0  29598  umgr2v2eedg  29611  umgr2v2e  29612  ifpsnprss  29709  upgriswlk  29727  clwwlkn1  30129  upgr1wlkdlem1  30233  1to2vfriswmgr  30367  esumpr2  34251  dvh2dim  41937  wopprc  43475  clsk1indlem4  44488  sge0prle  46844  meadjun  46905  elsprel  47950  sclnbgrelself  48339  upgrwlkupwlk  48631