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 12228

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 12220	. 2 class 8
2		c7 12219	. . 3 class 7
3		c1 11041	. . 3 class 1
4		caddc 11043	. . 3 class +
5	2, 3, 4	co 7370	. 2 class (7 + 1)
6	1, 5	wceq 1542	1 wff 8 = (7 + 1)

Colors of variables: wff setvar class

This definition is referenced by: 8nn 12254 8re 12255 8cn 12256 8pos 12271 8m1e7 12287 7p1e8 12303 4p4e8 12309 5p3e8 12311 6p2e8 12313 7p2e9 12315 7lt8 12346 8p8e16 12707 9p8e17 12714 9p9e18 12715 8t8e64 12742 9t8e72 12749 log2ub 26932 3cubeslem3r 43073 rmydioph 43400