HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Definition df-2 9191
Description: Define the number 2. (Contributed by NM, 27-May-1999.)
Assertion
Ref Expression
df-2  |-  2  =  ( 1  +  1 )

Detailed syntax breakdown of Definition df-2
StepHypRef Expression
1 c2 9182 . 2  class  2
2 c1 8165 . . 3  class  1
3 caddc 8167 . . 3  class  +
42, 2, 3co 5366 . 2  class  ( 1  +  1 )
51, 4wceq 1520 1  wff  2  =  ( 1  +  1 )
Colors of variables: wff set class
This definition is referenced by:  2re  9202  2pos  9215  1p1e2  9227  2p2e4  9228  2times  9229  3p2e5  9241  4p2e6  9243  5p2e7  9246  6p2e8  9250  7p2e9  9253  8p2e10  9255  2nn  9263  1lt2  9272  nneo  9479  6p6e12  9559  7p5e12  9561  8p4e12  9565  9p2e11  9570  9p3e12  9571  eluz2b1  9673  x2times  10002  fztp  10219  fzprval  10222  fztpval  10223  sqval  10533  fac2  10663  faclbnd4lem1  10675  bcp1m1  10701  hashprg  10736  iseralt  11364  binom11  11494  climcndslem1  11509  climcndslem2  11510  ege2le3  11570  ef4p  11592  efgt1p2  11593  eirrlem  11681  odd2np1lem  11784  isprm3  11888  prmind2  11890  opoe  11985  pockthlem  12073  pockthg  12074  prmunb  12082  prmreclem2  12085  4sqlem19  12131  vdwlem12  12160  decexp2  12211  swrds2  13173  mulg2  13302  efgs1b  13771  efgredlemc  13780  lt6abl  13906  abvtrivd  14330  pjthlem1  17498  ovolunlem1a  17552  ovolicc1  17572  vitalilem2  17661  itgcnlem  17841  dveflem  17997  coskpi  18489  ang180lem3  18611  tanatan  18786  cosatan  18788  atantayl2  18805  emcllem7  18866  basellem3  18891  basellem5  18893  basellem8  18896  issqf  18945  ppi2  18979  ppi3  18980  cht2  18981  ppieq0  18985  ppiublem2  19013  chpeq0  19018  chtublem  19021  chtub  19022  chpub  19030  mersenne  19037  perfectlem2  19040  bcp1ctr  19089  bclbnd  19090  bposlem1  19094  bposlem2  19095  bposlem6  19099  lgslem1  19106  lgsval2lem  19116  lgsdir2lem2  19134  lgsdir2lem3  19135  lgsdirprm  19139  lgseisen  19163  m1lgs  19172  rplogsumlem1  19204  rplogsumlem2  19205  dchrisum0flb  19230  dchrisum0re  19233  mulog2sumlem2  19255  pntrmax  19284  pntpbnd2  19307  pntibndlem2  19311  pntlemg  19318  pntlemr  19322  ex-fl  19385  1p1e2apr1  19390  vc2  19663  ipval2  19832  ip2i  19958  hv2times  20192  pjhthlem1  20522  ho2times  20951  stm1addi  21377  staddi  21378  stadd3i  21380  addltmulALT  21578  subfacp1lem1  21603  subfacp1lem5  21608  subfacp1lem6  21609  vdgr1d  21787  konigsberg  21804  axlowdimlem4  22467  axlowdimlem13  22476  bPoly1  22680  bpolydiflem  22683  intset  23882  pell14qrgapw  24752  rmydioph  24898  rmxdioph  24900  expdiophlem1  24905  expdiophlem2  24906  expdioph  24907  psgnunilem2  25252
Copyright terms: Public domain