Definition df-2 12141

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 12133	. 2 class 2
2		c1 10977	. . 3 class 1
3		caddc 10979	. . 3 class +
4	2, 2, 3	co 7341	. 2 class (1 + 1)
5	1, 4	wceq 1541	1 wff 2 = (1 + 1)

This definition is referenced by:  2nn  12151  2re  12152  2cn  12153  0le2  12180  2pos  12181  1p1e2  12203  2p2e4  12213  2times  12214  1p2e3  12221  3p2e5  12229  4p2e6  12231  5p2e7  12234  6p2e8  12237  7p2e9  12239  1lt2  12249  nneo  12509  6p6e12  12616  7p5e12  12619  8p2e10  12622  8p4e12  12624  9p2e11  12629  9p3e12  12630  5t2e10  12642  eluz2b1  12764  x2times  13138  fztp  13417  fz12pr  13418  fztpval  13423  fzo12sn  13575  fzosplitpr  13601  sqval  13940  fac2  14098  faclbnd4lem1  14112  bcp1m1  14139  hashprg  14214  hashgt23el  14243  hashge2el2difr  14299  swrds2  14752  iseralt  15495  binom11  15643  climcndslem1  15660  climcndslem2  15661  bpoly1  15860  bpolydiflem  15863  bpoly3  15867  bpoly4  15868  ege2le3  15898  ef4p  15921  efgt1p2  15922  eirrlem  16012  odd2np1lem  16148  opoe  16171  bitsfzolem  16240  isprm3  16485  prmind2  16487  dvdsnprmd  16492  2mulprm  16495  pockthlem  16703  pockthg  16704  prmunb  16712  prmreclem2  16715  4sqlem19  16761  vdwlem12  16790  prmgaplem8  16856  decexp2  16873  2expltfac  16891  gsumpr12val  18470  mulg2  18809  psgnunilem2  19199  efgs1b  19437  efgredlemc  19446  lt6abl  19590  abvtrivd  20205  m2detleiblem2  21882  clmvs2  24362  cphipval  24512  pjthlem1  24706  ovolunlem1a  24765  ovolicc1  24785  vitalilem2  24878  itgcnlem  25059  dveflem  25248  coskpi  25784  ang180lem3  26066  tanatan  26174  cosatan  26176  atantayl2  26193  emcllem7  26256  basellem3  26337  basellem5  26339  basellem8  26342  issqf  26390  ppi2  26424  ppi3  26425  cht2  26426  ppieq0  26430  ppiublem2  26456  chpeq0  26461  chtub  26465  chpub  26473  mersenne  26480  perfectlem2  26483  bcp1ctr  26532  bclbnd  26533  bposlem1  26537  bposlem2  26538  bposlem6  26542  lgslem1  26550  lgsval2lem  26560  lgsdir2lem2  26579  lgsdir2lem3  26580  lgsdirprm  26584  lgseisen  26632  m1lgs  26641  rplogsumlem1  26737  rplogsumlem2  26738  dchrisum0flb  26763  dchrisum0re  26766  mulog2sumlem2  26788  pntrmax  26817  pntpbnd2  26840  pntibndlem2  26844  pntlemg  26851  pntlemr  26855  axlowdimlem13  27610  clwlkclwwlklem2a  28649  1wlkdlem1  28788  upgr3v3e3cycl  28831  upgr4cycl4dv4e  28836  numclwlk2lem2f1o  29030  ex-fl  29098  1p1e2apr1  29117  vc2OLD  29217  ipval2  29356  ip2i  29477  hv2times  29710  pjhthlem1  30040  ho2times  30468  stm1addi  30894  staddi  30895  stadd3i  30897  addltmulALT  31095  threehalves  31474  usgrgt2cycl  33389  subfacp1lem1  33438  subfacp1lem5  33443  subfacp1lem6  33444  sin2h  35923  tan2h  35925  poimirlem25  35958  poimirlem27  35960  itg2addnclem3  35986  aks4d1p1p7  40387  facp2  40407  fac2xp3  40468  sn-1ne2  40606  remul02  40699  sn-0tie0  40732  3cubeslem3r  40822  pell14qrgapw  41011  rmydioph  41150  rmxdioph  41152  expdiophlem1  41157  expdiophlem2  41158  expdioph  41159  relexp2  41658  stoweidlem14  43943  wallispilem3  43996  wallispi2lem2  44001  fourierswlem  44159  perfectALTVlem2  45592  sbgoldbo  45657  nnsum3primes4  45658  nnsum3primesgbe  45662  difmodm1lt  46286  nnlog2ge0lt1  46330  itcoval2  46428  ackval2  46446  ackval42  46460