Definition df-2 8098

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 8089	. 2 class 2
2		c1 6982	. . 3 class 1
3		caddc 6984	. . 3 class +
4	2, 2, 3	co 5532	. 2 class ( 1 + 1 )
5	1, 4	wceq 1284	1 wff 2 = ( 1 + 1 )

This definition is referenced by:  2re  8109  0le2  8129  2pos  8130  1p1e2  8155  2p2e4  8159  2times  8160  3p2e5  8173  4p2e6  8175  5p2e7  8178  6p2e8  8181  7p2e9  8183  2nn  8193  1lt2  8201  nneoor  8449  6p6e12  8550  7p5e12  8553  8p2e10  8556  8p4e12  8558  9p2e11  8563  9p3e12  8564  5t2e10  8576  eluz2b1  8688  nn01to3  8702  fztp  9095  fzprval  9099  fztpval  9100  fzo12sn  9226  rebtwn2zlemstep  9261  rebtwn2z  9263  sqval  9534  fac2  9658  bcp1m1  9692  odd2np1lem  10271  opoe  10295  ncoprmgcdne1b  10471  isprm3  10500  prmind2  10502  dvdsnprmd  10507  prmgt1  10513  ex-fl  10563