Definition df-2 9366

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 9358	. 2 class 2
2		c1 8181	. . 3 class 1
3		caddc 8183	. . 3 class +
4	2, 2, 3	co 6085	. 2 class (1 + 1)
5	1, 4	wceq 1402	1 wff 2 = (1 + 1)

This definition is used by:  2re  9377  0le2  9397  2pos  9398  1p1e2  9424  2p2e4  9434  2times  9435  3p2e5  9449  4p2e6  9451  5p2e7  9454  6p2e8  9457  7p2e9  9459  2nn  9471  1lt2  9479  nneoor  9753  6p6e12  9860  7p5e12  9863  8p2e10  9866  8p4e12  9868  9p2e11  9873  9p3e12  9874  5t2e10  9886  eluz2b1  10011  nn01to3  10027  fztp  10496  fzprval  10500  fztpval  10501  fzo12sn  10646  fzosplitpr  10663  rebtwn2zlemstep  10698  rebtwn2z  10700  sqval  11049  fac2  11185  bcp1m1  11219  hashprg  11265  binom11  12272  ege2le3  12457  ef4p  12480  efgt1p2  12481  eirraplem  12563  odd2np1lem  12658  opoe  12681  bitsfzolem  12740  ncoprmgcdne1b  12886  isprm3  12915  prmind2  12917  dvdsnprmd  12922  prmgt1  12930  pockthlem  13158  pockthg  13159  prmunb  13164  4sqlem19  13211  2expltfac  13242  mulg2  13987  dveflem  15918  coskpi  16041  ppi2  16235  ppi3  16236  cht2  16237  ppiqeq0  16241  ppiublem2  16253  chtqub  16257  mersenne  16258  perfectlem2  16261  bcp1ctr  16267  bclbnd  16268  bposlem1  16272  bposlem2  16273  bposlem6  16277  lgslem1  16285  lgsval2lem  16295  lgsdir2lem2  16314  lgsdir2lem3  16315  lgsdirprm  16319  lgseisen  16359  m1lgs  16370  ex-fl  16905