Theorem dfsn2 4411

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 4401	. 2 ⊢ {𝐴, 𝐴} = ({𝐴} ∪ {𝐴})
2		unidm 3979	. 2 ⊢ ({𝐴} ∪ {𝐴}) = {𝐴}
3	1, 2	eqtr2i 2803	1 ⊢ {𝐴} = {𝐴, 𝐴}

Syntax hints:   = wceq 1601   ∪ cun 3790  {csn 4398  {cpr 4400

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-v 3400  df-un 3797  df-pr 4401

This theorem is referenced by:  nfsn  4474  disjprsn  4481  tpidm12  4522  tpidm  4525  ifpprsnss  4531  preqsnd  4620  preqsndOLD  4621  preqsnOLD  4625  elpreqprlem  4629  opidg  4655  unisng  4686  unisnOLD  4688  intsng  4745  snex  5140  opeqsng  5198  opeqsnOLD  5200  propeqop  5204  relop  5518  funopg  6169  f1oprswap  6434  fnprb  6744  enpr1g  8307  supsn  8666  infsn  8699  prdom2  9162  wuntp  9868  wunsn  9873  grusn  9961  prunioo  12618  hashprg  13497  hashfun  13538  hashle2pr  13573  lcmfsn  15754  lubsn  17480  indislem  21212  hmphindis  22009  wilthlem2  25247  upgrex  26440  umgrnloop0  26457  edglnl  26492  usgrnloop0ALT  26551  uspgr1v1eop  26596  1loopgruspgr  26848  1egrvtxdg0  26859  umgr2v2eedg  26872  umgr2v2e  26873  ifpsnprss  26970  upgriswlk  26988  clwwlkn1  27431  upgr1wlkdlem1  27548  1to2vfriswmgr  27687  esumpr2  30727  dvh2dim  37601  wopprc  38560  clsk1indlem4  39302  sge0prle  41546  meadjun  41607  elsprel  42418  upgrwlkupwlk  42767