df-9 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > df-9		Structured version Visualization version GIF version

Definition df-9 12256

Description: Define the number 9. (Contributed by NM, 27-May-1999.)

**Assertion**
Ref	Expression
df-9	⊢ 9 = (8 + 1)

**Detailed syntax breakdown of Definition df-9**
Step	Hyp	Ref	Expression
1		c9 12248	. 2 class 9
2		c8 12247	. . 3 class 8
3		c1 11069	. . 3 class 1
4		caddc 11071	. . 3 class +
5	2, 3, 4	co 7387	. 2 class (8 + 1)
6	1, 5	wceq 1540	1 wff 9 = (8 + 1)

Colors of variables: wff setvar class

This definition is referenced by: 9nn 12284 9re 12285 9cn 12286 9pos 12299 9m1e8 12315 8p1e9 12331 5p4e9 12339 6p3e9 12341 7p2e9 12342 8lt9 12380 8p2e10 12729 9p9e18 12743 9t9e81 12778 19prm 17088 139prm 17094 bposlem8 27202 lgsdir2lem5 27240 2lgsoddprmlem3d 27324 aks4d1p1 42064 rmydioph 43003 139prmALT 47597 9gbo 47775 wtgoldbnnsum4prm 47803 bgoldbnnsum3prm 47805