Theorem dfsn2 4595

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 4585	. 2 ⊢ {𝐴, 𝐴} = ({𝐴} ∪ {𝐴})
2		unidm 4110	. 2 ⊢ ({𝐴} ∪ {𝐴}) = {𝐴}
3	1, 2	eqtr2i 2786	1 ⊢ {𝐴} = {𝐴, 𝐴}

Syntax hints:   = wceq 1560   ∪ cun 3902  {csn 4582  {cpr 4584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-un 3909  df-pr 4585

This theorem is referenced by:  nfsn  4666  disjprsn  4673  tpidm12  4714  tpidm  4717  ifpprsnss  4723  preqsnd  4817  elpreqprlem  4824  opidg  4850  unisng  4883  intsng  4941  vsnex  5392  snex  5396  opeqsng  5472  propeqop  5476  relop  5822  funopg  6555  f1oprswap  6852  fnprb  7192  enpr1g  9004  prfi  9268  supsn  9419  infsn  9453  pr2ne  9961  prdom2  9962  wuntp  10669  wunsn  10674  grusn  10762  prunioo  13485  hashprg  14408  hashfun  14450  hashle2pr  14490  lcmfsn  16669  lubsn  18514  indislem  23057  hmphindis  23854  wilthlem2  27130  neg1s  28117  upgrex  29290  umgrnloop0  29307  edglnl  29341  usgrnloop0ALT  29403  uspgr1v1eop  29447  1loopgruspgr  29698  1egrvtxdg0  29709  umgr2v2eedg  29722  umgr2v2e  29723  ifpsnprss  29820  upgriswlk  29838  clwwlkn1  30240  upgr1wlkdlem1  30344  1to2vfriswmgr  30478  esumpr2  34361  dvh2dim  42066  wopprc  43604  clsk1indlem4  44617  sge0prle  46972  meadjun  47033  elsprel  48078  sclnbgrelself  48467  upgrwlkupwlk  48759