Theorem dfsn2 4604

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 4594	. 2 ⊢ {𝐴, 𝐴} = ({𝐴} ∪ {𝐴})
2		unidm 4111	. 2 ⊢ ({𝐴} ∪ {𝐴}) = {𝐴}
3	1, 2	eqtr2i 2789	1 ⊢ {𝐴} = {𝐴, 𝐴}

This proof depends on syntax axioms:   = wceq 1570   ∪ cun 3904  {csn 4591  {cpr 4593

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3911  df-pr 4594

This theorem is used by:  nfsn  4675  disjprsn  4682  tpidm12  4723  tpidm  4726  ifpprsnss  4732  preqsnd  4826  elpreqprlem  4833  opidg  4859  unisng  4892  intsng  4950  vsnex  5408  snex  5412  opeqsng  5488  propeqop  5492  relop  5838  funopg  6574  f1oprswap  6870  fnprb  7213  enpr1g  9026  prfi  9290  supsn  9440  infsn  9474  pr2ne  10005  prdom2  10006  wuntp  10711  wunsn  10716  grusn  10804  prunioo  13524  hashprg  14449  hashfun  14492  hashle2pr  14532  lcmfsn  16715  lubsn  18560  indislem  23207  hmphindis  24005  wilthlem2  27284  neg1s  28271  upgrex  29497  umgrnloop0  29514  edglnl  29548  usgrnloop0ALT  29613  uspgr1v1eop  29657  1loopgruspgr  29908  1egrvtxdg0  29919  umgr2v2eedg  29932  umgr2v2e  29933  ifpsnprss  30030  upgriswlk  30048  clwwlkn1  30459  upgr1wlkdlem1  30563  1to2vfriswmgr  30701  esumpr2  34521  dvh2dim  42277  wopprc  43815  clsk1indlem4  44828  sge0prle  47173  meadjun  47234  elsprel  48282  sclnbgrelself  48671  upgrwlkupwlk  48963