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

Definition df-2 10014
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 10005 . 2  class  2
2 c1 8947 . . 3  class  1
3 caddc 8949 . . 3  class  +
42, 2, 3co 6040 . 2  class  ( 1  +  1 )
51, 4wceq 1649 1  wff  2  =  ( 1  +  1 )
Colors of variables: wff set class
This definition is referenced by:  2re  10025  2pos  10038  1p1e2  10050  2p2e4  10054  2times  10055  3p2e5  10067  4p2e6  10069  5p2e7  10072  6p2e8  10076  7p2e9  10079  8p2e10  10081  2nn  10089  1lt2  10098  nneo  10309  6p6e12  10389  7p5e12  10391  8p4e12  10395  9p2e11  10400  9p3e12  10401  eluz2b1  10503  x2times  10834  fztp  11058  fzprval  11062  fztpval  11063  fzo12sn  11138  sqval  11396  fac2  11527  faclbnd4lem1  11539  bcp1m1  11566  hashprg  11621  swrds2  11835  iseralt  12433  binom11  12566  climcndslem1  12584  climcndslem2  12585  ege2le3  12647  ef4p  12669  efgt1p2  12670  eirrlem  12758  odd2np1lem  12862  bitsfzolem  12901  isprm3  13043  prmind2  13045  opoe  13140  pockthlem  13228  pockthg  13229  prmunb  13237  prmreclem2  13240  4sqlem19  13286  vdwlem12  13315  decexp2  13366  2expltfac  13381  mulg2  14854  efgs1b  15323  efgredlemc  15332  lt6abl  15459  abvtrivd  15883  pjthlem1  19291  ovolunlem1a  19345  ovolicc1  19365  vitalilem2  19454  itgcnlem  19634  dveflem  19816  coskpi  20381  ang180lem3  20606  tanatan  20712  cosatan  20714  atantayl2  20731  emcllem7  20793  basellem3  20818  basellem5  20820  basellem8  20823  issqf  20872  ppi2  20906  ppi3  20907  cht2  20908  ppieq0  20912  ppiublem2  20940  chpeq0  20945  chtub  20949  chpub  20957  mersenne  20964  perfectlem2  20967  bcp1ctr  21016  bclbnd  21017  bposlem1  21021  bposlem2  21022  bposlem6  21026  lgslem1  21033  lgsval2lem  21043  lgsdir2lem2  21061  lgsdir2lem3  21062  lgsdirprm  21066  lgseisen  21090  m1lgs  21099  rplogsumlem1  21131  rplogsumlem2  21132  dchrisum0flb  21157  dchrisum0re  21160  mulog2sumlem2  21182  pntrmax  21211  pntpbnd2  21234  pntibndlem2  21238  pntlemg  21245  pntlemr  21249  constr3trllem3  21592  constr3pthlem1  21595  constr3pthlem3  21597  vdgr1d  21627  konigsberg  21662  ex-fl  21708  1p1e2apr1  21713  vc2  21987  ipval2  22156  ip2i  22282  hv2times  22516  pjhthlem1  22846  ho2times  23275  stm1addi  23701  staddi  23702  stadd3i  23704  addltmulALT  23902  subfacp1lem1  24818  subfacp1lem5  24823  subfacp1lem6  24824  axlowdimlem4  25788  axlowdimlem13  25797  bpoly1  26001  bpolydiflem  26004  bpoly3  26008  bpoly4  26009  itg2addnclem3  26157  pell14qrgapw  26829  rmydioph  26975  rmxdioph  26977  expdiophlem1  26982  expdiophlem2  26983  expdioph  26984  psgnunilem2  27286  stoweidlem14  27630  wallispilem3  27683  wallispi2lem2  27688
  Copyright terms: Public domain W3C validator