Theorem dfsn2 4602

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

Syntax hints:   = wceq 1570   ∪ cun 3903  {csn 4589  {cpr 4591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3910  df-pr 4592

This theorem is referenced by:  nfsn  4673  disjprsn  4680  tpidm12  4721  tpidm  4724  ifpprsnss  4730  preqsnd  4824  elpreqprlem  4831  opidg  4857  unisng  4890  intsng  4948  vsnex  5406  snex  5410  opeqsng  5486  propeqop  5490  relop  5836  funopg  6570  f1oprswap  6866  fnprb  7206  enpr1g  9016  prfi  9279  supsn  9429  infsn  9463  pr2ne  9985  prdom2  9986  wuntp  10691  wunsn  10696  grusn  10784  prunioo  13503  hashprg  14427  hashfun  14470  hashle2pr  14510  lcmfsn  16688  lubsn  18533  indislem  23157  hmphindis  23954  wilthlem2  27233  neg1s  28220  upgrex  29442  umgrnloop0  29459  edglnl  29493  usgrnloop0ALT  29555  uspgr1v1eop  29599  1loopgruspgr  29850  1egrvtxdg0  29861  umgr2v2eedg  29874  umgr2v2e  29875  ifpsnprss  29972  upgriswlk  29990  clwwlkn1  30392  upgr1wlkdlem1  30496  1to2vfriswmgr  30630  esumpr2  34457  dvh2dim  42219  wopprc  43757  clsk1indlem4  44770  sge0prle  47115  meadjun  47176  elsprel  48224  sclnbgrelself  48613  upgrwlkupwlk  48905