MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dfsn2 Structured version   Visualization version   GIF version

Theorem dfsn2 4334
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
StepHypRef Expression
1 df-pr 4324 . 2 {𝐴, 𝐴} = ({𝐴} ∪ {𝐴})
2 unidm 3899 . 2 ({𝐴} ∪ {𝐴}) = {𝐴}
31, 2eqtr2i 2783 1 {𝐴} = {𝐴, 𝐴}
Colors of variables: wff setvar class
Syntax hints:   = wceq 1632  cun 3713  {csn 4321  {cpr 4323
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-v 3342  df-un 3720  df-pr 4324
This theorem is referenced by:  nfsn  4386  disjprsn  4394  tpidm12  4434  tpidm  4437  ifpprsnss  4443  preqsnd  4536  preqsndOLD  4537  preqsnOLD  4541  preqsnOLDOLD  4542  elpreqprlem  4546  opidg  4572  unisn  4603  intsng  4664  snex  5057  opeqsn  5115  propeqop  5118  relop  5428  funopg  6083  f1oprswap  6342  fnprb  6637  enpr1g  8189  supsn  8545  infsn  8577  prdom2  9039  wuntp  9745  wunsn  9750  grusn  9838  prunioo  12514  hashprg  13394  hashprgOLD  13395  hashfun  13436  hashle2pr  13471  lcmfsn  15570  lubsn  17315  indislem  21026  hmphindis  21822  wilthlem2  25015  upgrex  26207  umgrnloop0  26224  edglnl  26258  usgrnloop0ALT  26317  uspgr1v1eop  26361  1loopgruspgr  26627  1egrvtxdg0  26638  umgr2v2eedg  26651  umgr2v2e  26652  ifpsnprss  26749  upgriswlk  26768  clwwlkn1  27191  upgr1wlkdlem1  27318  1to2vfriswmgr  27454  esumpr2  30459  dvh2dim  37254  wopprc  38117  clsk1indlem4  38862  sge0prle  41139  meadjun  41200  upgrwlkupwlk  42249  elsprel  42253
  Copyright terms: Public domain W3C validator