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 12411

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 12403	. 2 class 8
2		c7 12402	. . 3 class 7
3		c1 11201	. . 3 class 1
4		caddc 11203	. . 3 class +
5	2, 3, 4	co 7420	. 2 class (7 + 1)
6	1, 5	wceq 1569	1 wff 8 = (7 + 1)

Colors of variables: wff setvar class

This definition is used by: 8nn 12438 8re 12439 8cn 12440 8m1e7 12475 7p1e8 12491 4p4e8 12497 5p3e8 12499 6p2e8 12501 7p2e9 12503 7lt8 12537 8p8e16 12905 9p8e17 12912 9p9e18 12913 8t8e64 12940 9t8e72 12947 log2ub 27277 1p8e9 43316 3cubeslem3r 43698 rmydioph 44021