Definition df-2 12275

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 12267	. 2 class 2
2		c1 11111	. . 3 class 1
3		caddc 11113	. . 3 class +
4	2, 2, 3	co 7409	. 2 class (1 + 1)
5	1, 4	wceq 1542	1 wff 2 = (1 + 1)

This definition is referenced by:  2nn  12285  2re  12286  2cn  12287  0le2  12314  2pos  12315  1p1e2  12337  2p2e4  12347  2times  12348  1p2e3  12355  3p2e5  12363  4p2e6  12365  5p2e7  12368  6p2e8  12371  7p2e9  12373  1lt2  12383  nneo  12646  6p6e12  12751  7p5e12  12754  8p2e10  12757  8p4e12  12759  9p2e11  12764  9p3e12  12765  5t2e10  12777  eluz2b1  12903  x2times  13278  fztp  13557  fz12pr  13558  fztpval  13563  fzo12sn  13715  fzosplitpr  13741  sqval  14080  fac2  14239  faclbnd4lem1  14253  bcp1m1  14280  hashprg  14355  hashgt23el  14384  hashge2el2difr  14442  swrds2  14891  iseralt  15631  binom11  15778  climcndslem1  15795  climcndslem2  15796  bpoly1  15995  bpolydiflem  15998  bpoly3  16002  bpoly4  16003  ege2le3  16033  ef4p  16056  efgt1p2  16057  eirrlem  16147  odd2np1lem  16283  opoe  16306  bitsfzolem  16375  isprm3  16620  prmind2  16622  dvdsnprmd  16627  2mulprm  16630  pockthlem  16838  pockthg  16839  prmunb  16847  prmreclem2  16850  4sqlem19  16896  vdwlem12  16925  prmgaplem8  16991  decexp2  17008  2expltfac  17026  gsumpr12val  18608  mulg2  18963  psgnunilem2  19363  efgs1b  19604  efgredlemc  19613  lt6abl  19763  abvtrivd  20448  m2detleiblem2  22130  clmvs2  24610  cphipval  24760  pjthlem1  24954  ovolunlem1a  25013  ovolicc1  25033  vitalilem2  25126  itgcnlem  25307  dveflem  25496  coskpi  26032  ang180lem3  26316  tanatan  26424  cosatan  26426  atantayl2  26443  emcllem7  26506  basellem3  26587  basellem5  26589  basellem8  26592  issqf  26640  ppi2  26674  ppi3  26675  cht2  26676  ppieq0  26680  ppiublem2  26706  chpeq0  26711  chtub  26715  chpub  26723  mersenne  26730  perfectlem2  26733  bcp1ctr  26782  bclbnd  26783  bposlem1  26787  bposlem2  26788  bposlem6  26792  lgslem1  26800  lgsval2lem  26810  lgsdir2lem2  26829  lgsdir2lem3  26830  lgsdirprm  26834  lgseisen  26882  m1lgs  26891  rplogsumlem1  26987  rplogsumlem2  26988  dchrisum0flb  27013  dchrisum0re  27016  mulog2sumlem2  27038  pntrmax  27067  pntpbnd2  27090  pntibndlem2  27094  pntlemg  27101  pntlemr  27105  axlowdimlem13  28212  clwlkclwwlklem2a  29251  1wlkdlem1  29390  upgr3v3e3cycl  29433  upgr4cycl4dv4e  29438  numclwlk2lem2f1o  29632  ex-fl  29700  1p1e2apr1  29719  vc2OLD  29821  ipval2  29960  ip2i  30081  hv2times  30314  pjhthlem1  30644  ho2times  31072  stm1addi  31498  staddi  31499  stadd3i  31501  addltmulALT  31699  threehalves  32081  usgrgt2cycl  34121  subfacp1lem1  34170  subfacp1lem5  34175  subfacp1lem6  34176  sin2h  36478  tan2h  36480  poimirlem25  36513  poimirlem27  36515  itg2addnclem3  36541  aks4d1p1p7  40939  facp2  40959  fac2xp3  41020  sn-1ne2  41179  remul02  41278  sn-0tie0  41312  3cubeslem3r  41425  pell14qrgapw  41614  rmydioph  41753  rmxdioph  41755  expdiophlem1  41760  expdiophlem2  41761  expdioph  41762  relexp2  42428  stoweidlem14  44730  wallispilem3  44783  wallispi2lem2  44788  fourierswlem  44946  perfectALTVlem2  46390  sbgoldbo  46455  nnsum3primes4  46456  nnsum3primesgbe  46460  difmodm1lt  47208  nnlog2ge0lt1  47252  itcoval2  47350  ackval2  47368  ackval42  47382