df-8 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > df-8		Structured version Visualization version GIF version

Definition df-8 10932

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 10923	. 2 class 8
2		c7 10922	. . 3 class 7
3		c1 9793	. . 3 class 1
4		caddc 9795	. . 3 class +
5	2, 3, 4	co 6527	. 2 class (7 + 1)
6	1, 5	wceq 1474	1 wff 8 = (7 + 1)

Colors of variables: wff setvar class

This definition is referenced by: 8re 10952 8pos 10968 8m1e7 10989 7p1e8 11004 4p4e8 11011 5p3e8 11013 6p2e8 11016 7p2e9 11019 8nn 11038 7lt8 11062 8p8e16 11450 9p8e17 11458 9p9e18 11459 8t8e64 11494 9t8e72 11501 log2ub 24393 lgsdir2lem1 24767 lgsdir2lem3 24769 rmydioph 36395