Theorem dfsn2 4639

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 4629	. 2 ⊢ {𝐴, 𝐴} = ({𝐴} ∪ {𝐴})
2		unidm 4157	. 2 ⊢ ({𝐴} ∪ {𝐴}) = {𝐴}
3	1, 2	eqtr2i 2766	1 ⊢ {𝐴} = {𝐴, 𝐴}

Syntax hints:   = wceq 1540   ∪ cun 3949  {csn 4626  {cpr 4628

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-un 3956  df-pr 4629

This theorem is referenced by:  nfsn  4707  disjprsn  4714  tpidm12  4755  tpidm  4758  ifpprsnss  4764  preqsnd  4859  elpreqprlem  4866  opidg  4892  unisng  4925  intsng  4983  vsnex  5434  opeqsng  5508  propeqop  5512  relop  5861  funopg  6600  f1oprswap  6892  fnprb  7228  enpr1g  9063  prfi  9363  supsn  9512  infsn  9545  pr2ne  10044  prdom2  10046  wuntp  10751  wunsn  10756  grusn  10844  prunioo  13521  hashprg  14434  hashfun  14476  hashle2pr  14516  lcmfsn  16672  lubsn  18527  indislem  23007  hmphindis  23805  wilthlem2  27112  negs1s  28059  upgrex  29109  umgrnloop0  29126  edglnl  29160  usgrnloop0ALT  29222  uspgr1v1eop  29266  1loopgruspgr  29518  1egrvtxdg0  29529  umgr2v2eedg  29542  umgr2v2e  29543  ifpsnprss  29641  upgriswlk  29659  clwwlkn1  30060  upgr1wlkdlem1  30164  1to2vfriswmgr  30298  esumpr2  34068  dvh2dim  41447  wopprc  43042  clsk1indlem4  44057  sge0prle  46416  meadjun  46477  elsprel  47462  sclnbgrelself  47834  upgrwlkupwlk  48056