Definition df-2 9049

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 9041	. 2 class 2
2		c1 7880	. . 3 class 1
3		caddc 7882	. . 3 class +
4	2, 2, 3	co 5922	. 2 class ( 1 + 1 )
5	1, 4	wceq 1364	1 wff 2 = ( 1 + 1 )

This definition is referenced by:  2re  9060  0le2  9080  2pos  9081  1p1e2  9107  2p2e4  9117  2times  9118  3p2e5  9132  4p2e6  9134  5p2e7  9137  6p2e8  9140  7p2e9  9142  2nn  9152  1lt2  9160  nneoor  9428  6p6e12  9530  7p5e12  9533  8p2e10  9536  8p4e12  9538  9p2e11  9543  9p3e12  9544  5t2e10  9556  eluz2b1  9675  nn01to3  9691  fztp  10153  fzprval  10157  fztpval  10158  fzo12sn  10293  rebtwn2zlemstep  10342  rebtwn2z  10344  sqval  10689  fac2  10823  bcp1m1  10857  hashprg  10900  binom11  11651  ege2le3  11836  ef4p  11859  efgt1p2  11860  eirraplem  11942  odd2np1lem  12037  opoe  12060  bitsfzolem  12118  ncoprmgcdne1b  12257  isprm3  12286  prmind2  12288  dvdsnprmd  12293  prmgt1  12300  pockthlem  12525  pockthg  12526  prmunb  12531  4sqlem19  12578  2expltfac  12608  gsumpr12val  13043  mulg2  13261  dveflem  14962  coskpi  15084  mersenne  15233  perfectlem2  15236  lgslem1  15241  lgsval2lem  15251  lgsdir2lem2  15270  lgsdir2lem3  15271  lgsdirprm  15275  lgseisen  15315  m1lgs  15326  ex-fl  15371