Theorem dfsn2 4598

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

Syntax hints:   = wceq 1540   ∪ cun 3909  {csn 4585  {cpr 4587

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-un 3916  df-pr 4588

This theorem is referenced by:  nfsn  4667  disjprsn  4674  tpidm12  4715  tpidm  4718  ifpprsnss  4724  preqsnd  4819  elpreqprlem  4826  opidg  4852  unisng  4885  intsng  4943  vsnex  5384  opeqsng  5458  propeqop  5462  relop  5804  funopg  6534  f1oprswap  6826  fnprb  7164  enpr1g  8971  prfi  9250  supsn  9400  infsn  9434  pr2ne  9933  prdom2  9935  wuntp  10640  wunsn  10645  grusn  10733  prunioo  13418  hashprg  14336  hashfun  14378  hashle2pr  14418  lcmfsn  16581  lubsn  18417  indislem  22863  hmphindis  23660  wilthlem2  26955  negs1s  27909  upgrex  28995  umgrnloop0  29012  edglnl  29046  usgrnloop0ALT  29108  uspgr1v1eop  29152  1loopgruspgr  29404  1egrvtxdg0  29415  umgr2v2eedg  29428  umgr2v2e  29429  ifpsnprss  29526  upgriswlk  29544  clwwlkn1  29943  upgr1wlkdlem1  30047  1to2vfriswmgr  30181  esumpr2  34030  dvh2dim  41412  wopprc  42992  clsk1indlem4  44006  sge0prle  46372  meadjun  46433  elsprel  47449  sclnbgrelself  47821  upgrwlkupwlk  48101