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 12307

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 12299	. 2 class 8
2		c7 12298	. . 3 class 7
3		c1 11128	. . 3 class 1
4		caddc 11130	. . 3 class +
5	2, 3, 4	co 7403	. 2 class (7 + 1)
6	1, 5	wceq 1540	1 wff 8 = (7 + 1)

Colors of variables: wff setvar class

This definition is referenced by: 8nn 12333 8re 12334 8cn 12335 8pos 12350 8m1e7 12371 7p1e8 12387 4p4e8 12393 5p3e8 12395 6p2e8 12397 7p2e9 12399 7lt8 12430 8p8e16 12792 9p8e17 12799 9p9e18 12800 8t8e64 12827 9t8e72 12834 log2ub 26909 3cubeslem3r 42657 rmydioph 42985