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

Definition df-2 8910
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 8901 . 2  class  2
2 c1 8138 . . 3  class  1
3 caddc 8140 . . 3  class  +
42, 2, 3co 5354 . 2  class  ( 1  +  1 )
51, 4wceq 1536 1  wff  2  =  ( 1  +  1 )
Colors of variables: wff set class
This definition is referenced by:  2re  8919  2pos  8930  1p1e2  8941  2p2e4  8942  2timesi  8943  3p2e5  8955  4p2e6  8957  5p2e7  8960  6p2e8  8964  7p2e9  8967  8p2e10  8969  2nn  8976  1lt2  8985  halfpos  9038  nneo  9178  6p6e12  9249  7p5e12  9251  8p4e12  9255  9p2e11  9260  9p3e12  9261  eluz2b1  9363  x2times  9624  fztp  9837  fzprval  9840  fztpval  9841  sqval  10133  fac2  10218  faclbnd4lem1  10230  bcp1m1  10255  hashpr  10289  iseralt  10747  binom11  10870  climcndslem1  10885  climcndslem2  10886  ege2le3  10943  ef4p  10964  efgt1p2  10965  eirrlem  11047  odd2np1lem  11150  isprm3  11253  prmind2  11255  opoe  11320  pockthlem  11407  pockthg  11408  prmunb  11416  prmreclem2  11419  4sqlem19  11465  vdwlem12  11494  decexp2  11545  snsnwolen  12348  swrdsnsn  12352  mulg2  12489  efgs1b  12804  efgredlemc  12811  abvtrivd  13227  pjthlem1  16517  ovolunlem1a  16571  ovolicc1  16591  vitalilem2  16680  itgcnlem  16860  dveflem  17015  coskpi  17485  ang180lem3  17591  tanatan  17724  cosatan  17726  atantayl2  17743  emcllem7  17795  basellem3  17813  basellem5  17815  basellem8  17818  issqf  17847  ppi2  17877  ppi3  17878  cht2  17879  ppieq0  17883  ppiublem2  17899  chtublem  17902  chtub  17903  bcp1ctr  17908  bclbnd  17909  bposlem1  17913  bposlem2  17914  bposlem6  17918  lgslem1  17925  lgsval2lem  17935  lgsdir2lem2  17953  lgsdir2lem3  17954  lgsdirprm  17958  lgseisen  17976  m1lgs  17985  ex-fl  18058  1p1e2apr1  18063  vc2  18332  ipval2  18501  ip2i  18627  hv2times  18861  pjhthlem1  19191  ho2times  19620  stm1addi  20046  staddi  20047  stadd3i  20049  addltmulALT  20247  subfacp1lem1  20272  subfacp1lem5  20277  subfacp1lem6  20278  vdgr1d  20460  konigsberg  20480  axlowdimlem4  21172  axlowdimlem13  21181  bPoly1  21385  bpolydiflem  21388  intset  22633  pell14qrgapw  23440  rmydioph  23590  rmxdioph  23592  expdiophlem1  23597  expdiophlem2  23598  expdioph  23599  psgnunilem2  23946
Copyright terms: Public domain