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

Definition df-2 8920
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 8911 . 2  class  2
2 c1 8148 . . 3  class  1
3 caddc 8150 . . 3  class  +
42, 2, 3co 5353 . 2  class  ( 1  +  1 )
51, 4wceq 1517 1  wff  2  =  ( 1  +  1 )
Colors of variables: wff set class
This definition is referenced by:  2re  8929  2pos  8940  1p1e2  8951  2p2e4  8952  2timesi  8953  3p2e5  8965  4p2e6  8967  5p2e7  8970  6p2e8  8974  7p2e9  8977  8p2e10  8979  2nn  8986  1lt2  8995  halfpos  9048  nneo  9188  6p6e12  9259  7p5e12  9261  8p4e12  9265  9p2e11  9270  9p3e12  9271  eluz2b1  9373  x2times  9637  fztp  9850  fzprval  9853  fztpval  9854  sqval  10147  fac2  10233  faclbnd4lem1  10245  bcp1m1  10270  hashpr  10305  iseralt  10775  binom11  10898  climcndslem1  10913  climcndslem2  10914  ege2le3  10971  ef4p  10992  efgt1p2  10993  eirrlem  11075  odd2np1lem  11178  isprm3  11281  prmind2  11283  opoe  11348  pockthlem  11435  pockthg  11436  prmunb  11444  prmreclem2  11447  4sqlem19  11493  vdwlem12  11522  decexp2  11573  swrds2  12465  mulg2  12593  efgs1b  12908  efgredlemc  12915  abvtrivd  13330  pjthlem1  16608  ovolunlem1a  16662  ovolicc1  16682  vitalilem2  16771  itgcnlem  16951  dveflem  17106  coskpi  17576  ang180lem3  17682  tanatan  17815  cosatan  17817  atantayl2  17834  emcllem7  17886  basellem3  17904  basellem5  17906  basellem8  17909  issqf  17938  ppi2  17968  ppi3  17969  cht2  17970  ppieq0  17974  ppiublem2  17990  chtublem  17993  chtub  17994  bcp1ctr  17999  bclbnd  18000  bposlem1  18004  bposlem2  18005  bposlem6  18009  lgslem1  18016  lgsval2lem  18026  lgsdir2lem2  18044  lgsdir2lem3  18045  lgsdirprm  18049  lgseisen  18067  m1lgs  18076  ex-fl  18149  1p1e2apr1  18154  vc2  18427  ipval2  18596  ip2i  18722  hv2times  18956  pjhthlem1  19286  ho2times  19715  stm1addi  20141  staddi  20142  stadd3i  20144  addltmulALT  20342  subfacp1lem1  20367  subfacp1lem5  20372  subfacp1lem6  20373  vdgr1d  20551  konigsberg  20568  konigsbergOLD  20569  axlowdimlem4  21254  axlowdimlem13  21263  bPoly1  21467  bpolydiflem  21470  intset  22731  pell14qrgapw  23536  rmydioph  23686  rmxdioph  23688  expdiophlem1  23693  expdiophlem2  23694  expdioph  23695  psgnunilem2  24042
Copyright terms: Public domain