Theorem dfsn2 4661

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

Syntax hints:   = wceq 1537   ∪ cun 3974  {csn 4648  {cpr 4650

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981  df-pr 4651

This theorem is referenced by:  nfsn  4732  disjprsn  4739  tpidm12  4780  tpidm  4783  ifpprsnss  4789  preqsnd  4883  elpreqprlem  4890  opidg  4916  unisng  4949  intsng  5007  vsnex  5449  opeqsng  5522  propeqop  5526  relop  5875  funopg  6612  f1oprswap  6906  fnprb  7245  enpr1g  9085  prfi  9391  supsn  9541  infsn  9574  pr2ne  10073  prdom2  10075  wuntp  10780  wunsn  10785  grusn  10873  prunioo  13541  hashprg  14444  hashfun  14486  hashle2pr  14526  lcmfsn  16682  lubsn  18552  indislem  23028  hmphindis  23826  wilthlem2  27130  negs1s  28077  upgrex  29127  umgrnloop0  29144  edglnl  29178  usgrnloop0ALT  29240  uspgr1v1eop  29284  1loopgruspgr  29536  1egrvtxdg0  29547  umgr2v2eedg  29560  umgr2v2e  29561  ifpsnprss  29659  upgriswlk  29677  clwwlkn1  30073  upgr1wlkdlem1  30177  1to2vfriswmgr  30311  esumpr2  34031  dvh2dim  41402  wopprc  42987  clsk1indlem4  44006  sge0prle  46322  meadjun  46383  elsprel  47349  sclnbgrelself  47720  upgrwlkupwlk  47863