Definition df-2 8419

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 8410	. 2 class 2
2		c1 7298	. . 3 class 1
3		caddc 7300	. . 3 class +
4	2, 2, 3	co 5615	. 2 class ( 1 + 1 )
5	1, 4	wceq 1287	1 wff 2 = ( 1 + 1 )

This definition is referenced by:  2re  8430  0le2  8450  2pos  8451  1p1e2  8476  2p2e4  8480  2times  8481  3p2e5  8494  4p2e6  8496  5p2e7  8499  6p2e8  8502  7p2e9  8504  2nn  8514  1lt2  8522  nneoor  8784  6p6e12  8885  7p5e12  8888  8p2e10  8891  8p4e12  8893  9p2e11  8898  9p3e12  8899  5t2e10  8911  eluz2b1  9023  nn01to3  9037  fztp  9425  fzprval  9429  fztpval  9430  fzo12sn  9559  rebtwn2zlemstep  9595  rebtwn2z  9597  sqval  9915  fac2  10039  bcp1m1  10073  hashprg  10116  odd2np1lem  10778  opoe  10801  ncoprmgcdne1b  10977  isprm3  11006  prmind2  11008  dvdsnprmd  11013  prmgt1  11019  ex-fl  11122