Theorem dfsn2 4596

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

This proof depends on syntax axioms:   = wceq 1569   ∪ cun 4149  {csn 4583  {cpr 4585

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 4151  df-pr 4586

This theorem is used by:  nfsn  4667  disjprsn  4674  tpidm12  4715  tpidm  4718  ifpprsnss  4724  preqsnd  4818  elpreqprlem  4825  opidg  4851  unisng  4884  intsng  4942  vsnex  5392  snex  5396  opeqsng  5474  propeqop  5478  relop  5827  funopg  6574  f1oprswap  6870  fnprb  7214  enpr1g  9050  prfi  9315  supsn  9465  infsn  9499  pr2ne  10084  prdom2  10085  wuntp  10796  wunsn  10801  grusn  10889  prunioo  13612  hashprg  14539  hashfun  14582  hashle2pr  14622  lcmfsn  16810  lubsn  18656  indislem  23318  hmphindis  24116  wilthlem2  27396  neg1s  28413  upgrex  29670  umgrnloop0  29687  edglnl  29721  usgrnloop0ALT  29786  uspgr1v1eop  29830  1loopgruspgr  30081  1egrvtxdg0  30092  umgr2v2eedg  30105  umgr2v2e  30106  ifpsnprss  30203  upgriswlk  30221  clwwlkn1  30632  upgr1wlkdlem1  30736  1to2vfriswmgr  30880  esumpr2  34699  dvh2dim  42503  wopprc  44037  clsk1indlem4  45044  sge0prle  47411  meadjun  47472  elsprel  48557  sclnbgrelself  48946  upgrwlkupwlk  49238