Theorem dfsn2 4593

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 4587	. 2 ⊢ {𝐴, 𝐴} = ({𝐴} ∪ {𝐴})
2		unidm 4155	. 2 ⊢ ({𝐴} ∪ {𝐴}) = {𝐴}
3	1, 2	eqtr2i 2784	1 ⊢ {𝐴} = {𝐴, 𝐴}

This proof depends on syntax axioms:   = wceq 1569   ∪ cun 4148  {csn 4584  {cpr 4586

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 4150  df-pr 4587

This theorem is used by:  nfsn  4664  disjprsn  4671  tpidm12  4712  tpidm  4715  ifpprsnss  4721  preqsnd  4813  elpreqprlem  4820  opidg  4851  unisng  4884  intsng  4942  vsnex  5393  snex  5397  opeqsng  5475  propeqop  5479  relop  5829  funopg  6579  f1oprswap  6875  fnprb  7218  enpr1g  9057  prfi  9322  supsn  9472  infsn  9506  pr2ne  10091  prdom2  10092  wuntp  10803  wunsn  10808  grusn  10896  prunioo  13619  hashprg  14546  hashfun  14589  hashle2pr  14629  lcmfsn  16819  lubsn  18665  indislem  23327  hmphindis  24125  wilthlem2  27405  neg1s  28422  upgrex  29679  umgrnloop0  29696  edglnl  29730  usgrnloop0ALT  29795  uspgr1v1eop  29839  1loopgruspgr  30090  1egrvtxdg0  30101  umgr2v2eedg  30114  umgr2v2e  30115  ifpsnprss  30212  upgriswlk  30230  clwwlkn1  30641  upgr1wlkdlem1  30745  1to2vfriswmgr  30889  esumpr2  34749  dvh2dim  42611  wopprc  44146  clsk1indlem4  45153  sge0prle  47519  meadjun  47580  elsprel  48665  sclnbgrelself  49054  upgrwlkupwlk  49346