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 12247

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 12239	. 2 class 8
2		c7 12238	. . 3 class 7
3		c1 11036	. . 3 class 1
4		caddc 11038	. . 3 class +
5	2, 3, 4	co 7364	. 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 12273 8re 12274 8cn 12275 8pos 12290 8m1e7 12306 7p1e8 12322 4p4e8 12328 5p3e8 12330 6p2e8 12332 7p2e9 12334 7lt8 12365 8p8e16 12727 9p8e17 12734 9p9e18 12735 8t8e64 12762 9t8e72 12769 log2ub 26910 3cubeslem3r 43116 rmydioph 43439