Definition df-8 9372

Description: Define the number 8. (Contributed by NM, 27-May-1999.)

Assertion

Ref	Expression
df-8	⊢ 8 = (7 + 1)

Detailed syntax breakdown of Definition df-8

Step	Hyp	Ref	Expression
1		c8 9364	. 2 class 8
2		c7 9363	. . 3 class 7
3		c1 8181	. . 3 class 1
4		caddc 8183	. . 3 class +
5	2, 3, 4	co 6085	. 2 class (7 + 1)
6	1, 5	wceq 1402	1 wff 8 = (7 + 1)

This definition is used by:  8re  9392  8pos  9410  8m1e7  9432  7p1e8  9447  4p4e8  9453  5p3e8  9455  6p2e8  9457  7p2e9  9459  8nn  9477  7lt8  9500  8p8e16  9872  9p8e17  9879  9p9e18  9880  8t8e64  9907  9t8e72  9914  log2ublog2  16147