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

Theorem dfsn2 4570
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 4560 . 2 {𝐴, 𝐴} = ({𝐴} ∪ {𝐴})
2 unidm 4125 . 2 ({𝐴} ∪ {𝐴}) = {𝐴}
31, 2eqtr2i 2842 1 {𝐴} = {𝐴, 𝐴}
Colors of variables: wff setvar class
Syntax hints:   = wceq 1528  cun 3931  {csn 4557  {cpr 4559
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-v 3494  df-un 3938  df-pr 4560
This theorem is referenced by:  nfsn  4635  disjprsn  4642  tpidm12  4683  tpidm  4686  ifpprsnss  4692  preqsnd  4781  elpreqprlem  4788  opidg  4814  unisng  4845  intsng  4902  snex  5322  opeqsng  5384  propeqop  5388  relop  5714  funopg  6382  f1oprswap  6651  fnprb  6962  enpr1g  8563  supsn  8924  infsn  8957  prdom2  9420  wuntp  10121  wunsn  10126  grusn  10214  prunioo  12855  hashprg  13744  hashfun  13786  hashle2pr  13823  lcmfsn  15967  lubsn  17692  indislem  21536  hmphindis  22333  wilthlem2  25573  upgrex  26804  umgrnloop0  26821  edglnl  26855  usgrnloop0ALT  26914  uspgr1v1eop  26958  1loopgruspgr  27209  1egrvtxdg0  27220  umgr2v2eedg  27233  umgr2v2e  27234  ifpsnprss  27331  upgriswlk  27349  clwwlkn1  27746  upgr1wlkdlem1  27851  1to2vfriswmgr  27985  esumpr2  31225  dvh2dim  38461  wopprc  39505  clsk1indlem4  40272  sge0prle  42560  meadjun  42621  elsprel  43514  upgrwlkupwlk  43892
  Copyright terms: Public domain W3C validator