MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-2 Unicode version

Definition df-2 9220
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 9211 . 2  class  2
2 c1 8194 . . 3  class  1
3 caddc 8196 . . 3  class  +
42, 2, 3co 5395 . 2  class  ( 1  +  1 )
51, 4wceq 1525 1  wff  2  =  ( 1  +  1 )
Colors of variables: wff set class
This definition is referenced by:  2re  9231  2pos  9244  1p1e2  9256  2p2e4  9257  2times  9258  3p2e5  9270  4p2e6  9272  5p2e7  9275  6p2e8  9279  7p2e9  9282  8p2e10  9284  2nn  9292  1lt2  9301  nneo  9508  6p6e12  9588  7p5e12  9590  8p4e12  9594  9p2e11  9599  9p3e12  9600  eluz2b1  9702  x2times  10031  fztp  10248  fzprval  10251  fztpval  10252  sqval  10562  fac2  10692  faclbnd4lem1  10704  bcp1m1  10730  hashprg  10765  iseralt  11393  binom11  11523  climcndslem1  11538  climcndslem2  11539  ege2le3  11599  ef4p  11621  efgt1p2  11622  eirrlem  11710  odd2np1lem  11813  isprm3  11917  prmind2  11919  opoe  12014  pockthlem  12102  pockthg  12103  prmunb  12111  prmreclem2  12114  4sqlem19  12160  vdwlem12  12189  decexp2  12240  swrds2  13202  mulg2  13331  efgs1b  13800  efgredlemc  13809  lt6abl  13935  abvtrivd  14359  pjthlem1  17527  ovolunlem1a  17581  ovolicc1  17601  vitalilem2  17690  itgcnlem  17870  dveflem  18026  coskpi  18518  ang180lem3  18640  tanatan  18815  cosatan  18817  atantayl2  18834  emcllem7  18895  basellem3  18920  basellem5  18922  basellem8  18925  issqf  18974  ppi2  19008  ppi3  19009  cht2  19010  ppieq0  19014  ppiublem2  19042  chpeq0  19047  chtublem  19050  chtub  19051  chpub  19059  mersenne  19066  perfectlem2  19069  bcp1ctr  19118  bclbnd  19119  bposlem1  19123  bposlem2  19124  bposlem6  19128  lgslem1  19135  lgsval2lem  19145  lgsdir2lem2  19163  lgsdir2lem3  19164  lgsdirprm  19168  lgseisen  19192  m1lgs  19201  rplogsumlem1  19233  rplogsumlem2  19234  dchrisum0flb  19259  dchrisum0re  19262  mulog2sumlem2  19284  pntrmax  19313  pntpbnd2  19336  pntibndlem2  19340  pntlemg  19347  pntlemr  19351  ex-fl  19414  1p1e2apr1  19419  vc2  19692  ipval2  19861  ip2i  19987  hv2times  20221  pjhthlem1  20551  ho2times  20980  stm1addi  21406  staddi  21407  stadd3i  21409  addltmulALT  21607  subfacp1lem1  21632  subfacp1lem5  21637  subfacp1lem6  21638  vdgr1d  21816  konigsberg  21833  axlowdimlem4  22496  axlowdimlem13  22505  bPoly1  22709  bpolydiflem  22712  intset  23915  pell14qrgapw  24815  rmydioph  24961  rmxdioph  24963  expdiophlem1  24968  expdiophlem2  24969  expdioph  24970  psgnunilem2  25315
  Copyright terms: Public domain W3C validator