Definition df-8 12288

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 12280	. 2 class 8
2		c7 12279	. . 3 class 7
3		c1 11076	. . 3 class 1
4		caddc 11078	. . 3 class +
5	2, 3, 4	co 7398	. 2 class (7 + 1)
6	1, 5	wceq 1562	1 wff 8 = (7 + 1)

This definition is referenced by:  8nn  12315  8re  12316  8cn  12317  8m1e7  12352  7p1e8  12368  4p4e8  12374  5p3e8  12376  6p2e8  12378  7p2e9  12380  7lt8  12414  8p8e16  12781  9p8e17  12788  9p9e18  12789  8t8e64  12816  9t8e72  12823  log2ub  27016  3cubeslem3r  43273  rmydioph  43596