Definition df-2 7733

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 7724	. 2 class 2
2		c1 6692	. . 3 class 1
3		caddc 6694	. . 3 class +
4	2, 2, 3	co 5455	. 2 class (1 + 1)
5	1, 4	wceq 1242	1 wff 2 = (1 + 1)

This definition is referenced by:  2re  7745  0le2  7766  2pos  7767  1p1e2  7791  2p2e4  7795  2times  7796  3p2e5  7810  4p2e6  7812  5p2e7  7815  6p2e8  7819  7p2e9  7822  8p2e10  7824  2nn  7835  1lt2  7844  nneoor  8096  6p6e12  8174  7p5e12  8176  8p4e12  8180  9p2e11  8185  9p3e12  8186  eluz2b1  8295  nn01to3  8308  fztp  8690  fzprval  8694  fztpval  8695  fzo12sn  8823  sqval  8946