Theorem dfsn2 4607

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 4597	. 2 ⊢ {𝐴, 𝐴} = ({𝐴} ∪ {𝐴})
2		unidm 4119	. 2 ⊢ ({𝐴} ∪ {𝐴}) = {𝐴}
3	1, 2	eqtr2i 2793	1 ⊢ {𝐴} = {𝐴, 𝐴}

Syntax hints:   = wceq 1567   ∪ cun 3911  {csn 4594  {cpr 4596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-un 3918  df-pr 4597

This theorem is referenced by:  nfsn  4678  disjprsn  4685  tpidm12  4726  tpidm  4729  ifpprsnss  4735  preqsnd  4828  elpreqprlem  4835  opidg  4861  unisng  4894  intsng  4952  vsnex  5407  snex  5411  opeqsng  5487  propeqop  5491  relop  5837  funopg  6571  f1oprswap  6867  fnprb  7207  enpr1g  9019  prfi  9282  supsn  9432  infsn  9466  pr2ne  9988  prdom2  9989  wuntp  10695  wunsn  10700  grusn  10788  prunioo  13507  hashprg  14430  hashfun  14473  hashle2pr  14513  lcmfsn  16692  lubsn  18537  indislem  23125  hmphindis  23922  wilthlem2  27198  neg1s  28185  upgrex  29382  umgrnloop0  29399  edglnl  29433  usgrnloop0ALT  29495  uspgr1v1eop  29539  1loopgruspgr  29790  1egrvtxdg0  29801  umgr2v2eedg  29814  umgr2v2e  29815  ifpsnprss  29912  upgriswlk  29930  clwwlkn1  30332  upgr1wlkdlem1  30436  1to2vfriswmgr  30570  esumpr2  34401  dvh2dim  42108  wopprc  43648  clsk1indlem4  44661  sge0prle  47006  meadjun  47067  elsprel  48112  sclnbgrelself  48501  upgrwlkupwlk  48793