Theorem dfsn2 4526

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 4516	. 2 ⊢ {𝐴, 𝐴} = ({𝐴} ∪ {𝐴})
2		unidm 4040	. 2 ⊢ ({𝐴} ∪ {𝐴}) = {𝐴}
3	1, 2	eqtr2i 2762	1 ⊢ {𝐴} = {𝐴, 𝐴}

Syntax hints:   = wceq 1542   ∪ cun 3839  {csn 4513  {cpr 4515

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-tru 1545  df-ex 1787  df-sb 2074  df-clab 2717  df-cleq 2730  df-clel 2811  df-v 3399  df-un 3846  df-pr 4516

This theorem is referenced by:  nfsn  4595  disjprsn  4602  tpidm12  4643  tpidm  4646  ifpprsnss  4652  preqsnd  4741  elpreqprlem  4748  opidg  4777  unisng  4814  intsng  4870  snex  5295  opeqsng  5357  propeqop  5361  relop  5687  funopg  6367  f1oprswap  6655  fnprb  6975  enpr1g  8615  supsn  9002  infsn  9035  prdom2  9499  wuntp  10204  wunsn  10209  grusn  10297  prunioo  12948  hashprg  13841  hashfun  13883  hashle2pr  13922  lcmfsn  16069  lubsn  17813  indislem  21744  hmphindis  22541  wilthlem2  25798  upgrex  27029  umgrnloop0  27046  edglnl  27080  usgrnloop0ALT  27139  uspgr1v1eop  27183  1loopgruspgr  27434  1egrvtxdg0  27445  umgr2v2eedg  27458  umgr2v2e  27459  ifpsnprss  27556  upgriswlk  27574  clwwlkn1  27970  upgr1wlkdlem1  28074  1to2vfriswmgr  28208  esumpr2  31597  dvh2dim  39071  wopprc  40408  clsk1indlem4  41184  sge0prle  43465  meadjun  43526  elsprel  44445  upgrwlkupwlk  44820