Definition df-2 12036

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 12028	. 2 class 2
2		c1 10872	. . 3 class 1
3		caddc 10874	. . 3 class +
4	2, 2, 3	co 7275	. 2 class (1 + 1)
5	1, 4	wceq 1539	1 wff 2 = (1 + 1)

This definition is referenced by:  2nn  12046  2re  12047  2cn  12048  0le2  12075  2pos  12076  1p1e2  12098  2p2e4  12108  2times  12109  1p2e3  12116  3p2e5  12124  4p2e6  12126  5p2e7  12129  6p2e8  12132  7p2e9  12134  1lt2  12144  nneo  12404  6p6e12  12511  7p5e12  12514  8p2e10  12517  8p4e12  12519  9p2e11  12524  9p3e12  12525  5t2e10  12537  eluz2b1  12659  x2times  13033  fztp  13312  fz12pr  13313  fztpval  13318  fzo12sn  13470  fzosplitpr  13496  sqval  13835  fac2  13993  faclbnd4lem1  14007  bcp1m1  14034  hashprg  14110  hashgt23el  14139  hashge2el2difr  14195  swrds2  14653  iseralt  15396  binom11  15544  climcndslem1  15561  climcndslem2  15562  bpoly1  15761  bpolydiflem  15764  bpoly3  15768  bpoly4  15769  ege2le3  15799  ef4p  15822  efgt1p2  15823  eirrlem  15913  odd2np1lem  16049  opoe  16072  bitsfzolem  16141  isprm3  16388  prmind2  16390  dvdsnprmd  16395  2mulprm  16398  pockthlem  16606  pockthg  16607  prmunb  16615  prmreclem2  16618  4sqlem19  16664  vdwlem12  16693  prmgaplem8  16759  decexp2  16776  2expltfac  16794  gsumpr12val  18373  mulg2  18713  psgnunilem2  19103  efgs1b  19342  efgredlemc  19351  lt6abl  19496  abvtrivd  20100  m2detleiblem2  21777  clmvs2  24257  cphipval  24407  pjthlem1  24601  ovolunlem1a  24660  ovolicc1  24680  vitalilem2  24773  itgcnlem  24954  dveflem  25143  coskpi  25679  ang180lem3  25961  tanatan  26069  cosatan  26071  atantayl2  26088  emcllem7  26151  basellem3  26232  basellem5  26234  basellem8  26237  issqf  26285  ppi2  26319  ppi3  26320  cht2  26321  ppieq0  26325  ppiublem2  26351  chpeq0  26356  chtub  26360  chpub  26368  mersenne  26375  perfectlem2  26378  bcp1ctr  26427  bclbnd  26428  bposlem1  26432  bposlem2  26433  bposlem6  26437  lgslem1  26445  lgsval2lem  26455  lgsdir2lem2  26474  lgsdir2lem3  26475  lgsdirprm  26479  lgseisen  26527  m1lgs  26536  rplogsumlem1  26632  rplogsumlem2  26633  dchrisum0flb  26658  dchrisum0re  26661  mulog2sumlem2  26683  pntrmax  26712  pntpbnd2  26735  pntibndlem2  26739  pntlemg  26746  pntlemr  26750  axlowdimlem13  27322  clwlkclwwlklem2a  28362  1wlkdlem1  28501  upgr3v3e3cycl  28544  upgr4cycl4dv4e  28549  numclwlk2lem2f1o  28743  ex-fl  28811  1p1e2apr1  28830  vc2OLD  28930  ipval2  29069  ip2i  29190  hv2times  29423  pjhthlem1  29753  ho2times  30181  stm1addi  30607  staddi  30608  stadd3i  30610  addltmulALT  30808  threehalves  31189  usgrgt2cycl  33092  subfacp1lem1  33141  subfacp1lem5  33146  subfacp1lem6  33147  sin2h  35767  tan2h  35769  poimirlem25  35802  poimirlem27  35804  itg2addnclem3  35830  aks4d1p1p7  40082  facp2  40099  fac2xp3  40160  sn-1ne2  40295  remul02  40388  sn-0tie0  40421  3cubeslem3r  40509  pell14qrgapw  40698  rmydioph  40836  rmxdioph  40838  expdiophlem1  40843  expdiophlem2  40844  expdioph  40845  relexp2  41285  stoweidlem14  43555  wallispilem3  43608  wallispi2lem2  43613  fourierswlem  43771  perfectALTVlem2  45174  sbgoldbo  45239  nnsum3primes4  45240  nnsum3primesgbe  45244  difmodm1lt  45868  nnlog2ge0lt1  45912  itcoval2  46010  ackval2  46028  ackval42  46042