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 12051

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 12043	. 2 class 8
2		c7 12042	. . 3 class 7
3		c1 10881	. . 3 class 1
4		caddc 10883	. . 3 class +
5	2, 3, 4	co 7284	. 2 class (7 + 1)
6	1, 5	wceq 1539	1 wff 8 = (7 + 1)

Colors of variables: wff setvar class

This definition is referenced by: 8nn 12077 8re 12078 8cn 12079 8pos 12094 8m1e7 12115 7p1e8 12131 4p4e8 12137 5p3e8 12139 6p2e8 12141 7p2e9 12143 7lt8 12174 8p8e16 12532 9p8e17 12539 9p9e18 12540 8t8e64 12567 9t8e72 12574 log2ub 26108 3cubeslem3r 40516 rmydioph 40843