Definition df-2 9066

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 9058	. 2 class 2
2		c1 7897	. . 3 class 1
3		caddc 7899	. . 3 class +
4	2, 2, 3	co 5925	. 2 class (1 + 1)
5	1, 4	wceq 1364	1 wff 2 = (1 + 1)

This definition is referenced by:  2re  9077  0le2  9097  2pos  9098  1p1e2  9124  2p2e4  9134  2times  9135  3p2e5  9149  4p2e6  9151  5p2e7  9154  6p2e8  9157  7p2e9  9159  2nn  9169  1lt2  9177  nneoor  9445  6p6e12  9547  7p5e12  9550  8p2e10  9553  8p4e12  9555  9p2e11  9560  9p3e12  9561  5t2e10  9573  eluz2b1  9692  nn01to3  9708  fztp  10170  fzprval  10174  fztpval  10175  fzo12sn  10310  rebtwn2zlemstep  10359  rebtwn2z  10361  sqval  10706  fac2  10840  bcp1m1  10874  hashprg  10917  binom11  11668  ege2le3  11853  ef4p  11876  efgt1p2  11877  eirraplem  11959  odd2np1lem  12054  opoe  12077  bitsfzolem  12136  ncoprmgcdne1b  12282  isprm3  12311  prmind2  12313  dvdsnprmd  12318  prmgt1  12325  pockthlem  12550  pockthg  12551  prmunb  12556  4sqlem19  12603  2expltfac  12633  gsumpr12val  13102  mulg2  13337  dveflem  15046  coskpi  15168  mersenne  15317  perfectlem2  15320  lgslem1  15325  lgsval2lem  15335  lgsdir2lem2  15354  lgsdir2lem3  15355  lgsdirprm  15359  lgseisen  15399  m1lgs  15410  ex-fl  15455