Theorem dfsn2 4190

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 4180	. 2 ⊢ {𝐴, 𝐴} = ({𝐴} ∪ {𝐴})
2		unidm 3756	. 2 ⊢ ({𝐴} ∪ {𝐴}) = {𝐴}
3	1, 2	eqtr2i 2645	1 ⊢ {𝐴} = {𝐴, 𝐴}

Syntax hints:   = wceq 1483   ∪ cun 3572  {csn 4177  {cpr 4179

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-un 3579  df-pr 4180

This theorem is referenced by:  nfsn  4242  disjprsn  4250  tpidm12  4290  tpidm  4293  ifpprsnss  4299  preqsnd  4392  preqsn  4393  preqsnOLD  4394  elpreqprlem  4395  opid  4421  unisn  4451  intsng  4512  snex  4908  opeqsn  4967  propeqop  4970  relop  5272  funopg  5922  f1oprswap  6180  fnprb  6472  enpr1g  8022  supsn  8378  infsn  8410  prdom2  8829  wuntp  9533  wunsn  9538  grusn  9626  prunioo  12301  hashprg  13182  hashprgOLD  13183  hashfun  13224  hashle2pr  13259  lcmfsn  15348  lubsn  17094  indislem  20804  hmphindis  21600  wilthlem2  24795  upgrex  25987  umgrnloop0  26004  edglnl  26038  usgrnloop0ALT  26097  uspgr1v1eop  26141  1loopgruspgr  26396  1egrvtxdg0  26407  umgr2v2eedg  26420  umgr2v2e  26421  ifpsnprss  26518  upgriswlk  26537  upgr1wlkdlem1  27005  1to2vfriswmgr  27143  esumpr2  30129  opidORIG  34109  dvh2dim  36734  wopprc  37597  clsk1indlem4  38342  sge0prle  40618  meadjun  40679  opidg  41297  upgrwlkupwlk  41721  elsprel  41725