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 12218

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 12210	. 2 class 8
2		c7 12209	. . 3 class 7
3		c1 11031	. . 3 class 1
4		caddc 11033	. . 3 class +
5	2, 3, 4	co 7360	. 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 12244 8re 12245 8cn 12246 8pos 12261 8m1e7 12277 7p1e8 12293 4p4e8 12299 5p3e8 12301 6p2e8 12303 7p2e9 12305 7lt8 12336 8p8e16 12697 9p8e17 12704 9p9e18 12705 8t8e64 12732 9t8e72 12739 log2ub 26919 3cubeslem3r 42996 rmydioph 43323