Definition df-8 12245

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 12237	. 2 class 8
2		c7 12236	. . 3 class 7
3		c1 11035	. . 3 class 1
4		caddc 11037	. . 3 class +
5	2, 3, 4	co 7359	. 2 class (7 + 1)
6	1, 5	wceq 1548	1 wff 8 = (7 + 1)

This definition is referenced by:  8nn  12271  8re  12272  8cn  12273  8pos  12288  8m1e7  12304  7p1e8  12320  4p4e8  12326  5p3e8  12328  6p2e8  12330  7p2e9  12332  7lt8  12363  8p8e16  12725  9p8e17  12732  9p9e18  12733  8t8e64  12760  9t8e72  12767  log2ub  26934  3cubeslem3r  43149  rmydioph  43472