Definition df-2 11284

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

Step	Hyp	Ref	Expression
1		c2 11275	. 2 class 2
2		c1 10142	. . 3 class 1
3		caddc 10144	. . 3 class +
4	2, 2, 3	co 6795	. 2 class (1 + 1)
5	1, 4	wceq 1631	1 wff 2 = (1 + 1)

This definition is referenced by:  2re  11295  0le2  11316  2pos  11317  1p1e2  11340  2p2e4  11350  2times  11351  3p2e5  11366  4p2e6  11368  5p2e7  11371  6p2e8  11375  7p2e9  11378  8p2e10OLD  11380  2nn  11391  1lt2  11400  nneo  11667  6p6e12  11807  7p5e12  11812  8p2e10  11815  8p4e12  11819  9p2e11  11824  9p2e11OLD  11825  9p3e12  11826  5t2e10  11839  eluz2b1  11966  x2times  12333  fztp  12603  fzprval  12607  fztpval  12608  fzo12sn  12758  fzosplitpr  12784  sqval  13128  fac2  13269  faclbnd4lem1  13283  bcp1m1  13310  hashprg  13383  hashprgOLD  13384  hashge2el2difr  13464  swrds2  13893  iseralt  14622  binom11  14770  climcndslem1  14787  climcndslem2  14788  bpoly1  14987  bpolydiflem  14990  bpoly3  14994  bpoly4  14995  ege2le3  15025  ef4p  15048  efgt1p2  15049  eirrlem  15137  odd2np1lem  15271  opoe  15294  bitsfzolem  15363  isprm3  15602  prmind2  15604  dvdsnprmd  15609  prmgt1  15615  pockthlem  15815  pockthg  15816  prmunb  15824  prmreclem2  15827  4sqlem19  15873  vdwlem12  15902  prmgaplem8  15968  decexp2  15985  2expltfac  16005  gsumpr12val  17489  mulg2  17757  psgnunilem2  18121  efgs1b  18355  efgredlemc  18364  lt6abl  18502  abvtrivd  19049  m2detleiblem2  20651  clmvs2  23112  cphipval  23260  pjthlem1  23426  ovolunlem1a  23483  ovolicc1  23503  vitalilem2  23596  itgcnlem  23775  dveflem  23961  coskpi  24492  ang180lem3  24761  tanatan  24866  cosatan  24868  atantayl2  24885  emcllem7  24948  basellem3  25029  basellem5  25031  basellem8  25034  issqf  25082  ppi2  25116  ppi3  25117  cht2  25118  ppieq0  25122  ppiublem2  25148  chpeq0  25153  chtub  25157  chpub  25165  mersenne  25172  perfectlem2  25175  bcp1ctr  25224  bclbnd  25225  bposlem1  25229  bposlem2  25230  bposlem6  25234  lgslem1  25242  lgsval2lem  25252  lgsdir2lem2  25271  lgsdir2lem3  25272  lgsdirprm  25276  lgseisen  25324  m1lgs  25333  rplogsumlem1  25393  rplogsumlem2  25394  dchrisum0flb  25419  dchrisum0re  25422  mulog2sumlem2  25444  pntrmax  25473  pntpbnd2  25496  pntibndlem2  25500  pntlemg  25507  pntlemr  25511  axlowdimlem4  26045  axlowdimlem13  26054  clwlkclwwlklem2a  27147  1wlkdlem1  27316  upgr3v3e3cycl  27359  upgr4cycl4dv4e  27364  numclwlk2lem2f1o  27569  numclwlk2lem2f1oOLD  27576  ex-fl  27645  1p1e2apr1  27663  vc2OLD  27762  ipval2  27901  ip2i  28022  hv2times  28257  pjhthlem1  28589  ho2times  29017  stm1addi  29443  staddi  29444  stadd3i  29446  addltmulALT  29644  threehalves  29962  subfacp1lem1  31498  subfacp1lem5  31503  subfacp1lem6  31504  sin2h  33731  tan2h  33733  poimirlem25  33766  poimirlem27  33768  itg2addnclem3  33794  pell14qrgapw  37966  rmydioph  38107  rmxdioph  38109  expdiophlem1  38114  expdiophlem2  38115  expdioph  38116  relexp2  38495  stoweidlem14  40745  wallispilem3  40798  wallispi2lem2  40803  fourierswlem  40961  perfectALTVlem2  42156  sbgoldbo  42200  nnsum3primes4  42201  nnsum3primesgbe  42205  difmodm1lt  42842  nnlog2ge0lt1  42885