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

Theorem dfsn2 4298
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 4288 . 2 {𝐴, 𝐴} = ({𝐴} ∪ {𝐴})
2 unidm 3864 . 2 ({𝐴} ∪ {𝐴}) = {𝐴}
31, 2eqtr2i 2747 1 {𝐴} = {𝐴, 𝐴}
Colors of variables: wff setvar class
Syntax hints:   = wceq 1596  cun 3678  {csn 4285  {cpr 4287
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-v 3306  df-un 3685  df-pr 4288
This theorem is referenced by:  nfsn  4349  disjprsn  4357  tpidm12  4397  tpidm  4400  ifpprsnss  4406  preqsnd  4499  preqsn  4500  preqsnOLD  4501  elpreqprlem  4502  opidg  4528  unisn  4559  intsng  4620  snex  5013  opeqsn  5071  propeqop  5074  relop  5380  funopg  6035  f1oprswap  6293  fnprb  6588  enpr1g  8138  supsn  8494  infsn  8526  prdom2  8942  wuntp  9646  wunsn  9651  grusn  9739  prunioo  12415  hashprg  13295  hashprgOLD  13296  hashfun  13337  hashle2pr  13372  lcmfsn  15471  lubsn  17216  indislem  20927  hmphindis  21723  wilthlem2  24915  upgrex  26107  umgrnloop0  26124  edglnl  26158  usgrnloop0ALT  26217  uspgr1v1eop  26261  1loopgruspgr  26527  1egrvtxdg0  26538  umgr2v2eedg  26551  umgr2v2e  26552  ifpsnprss  26649  upgriswlk  26668  clwwlkn1  27091  upgr1wlkdlem1  27218  1to2vfriswmgr  27354  esumpr2  30359  dvh2dim  37153  wopprc  38016  clsk1indlem4  38761  sge0prle  41038  meadjun  41099  upgrwlkupwlk  42148  elsprel  42152
  Copyright terms: Public domain W3C validator