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 12315

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 12307	. 2 class 9
2		c8 12306	. . 3 class 8
3		c1 11141	. . 3 class 1
4		caddc 11143	. . 3 class +
5	2, 3, 4	co 7419	. 2 class (8 + 1)
6	1, 5	wceq 1533	1 wff 9 = (8 + 1)

Colors of variables: wff setvar class

This definition is referenced by: 9nn 12343 9re 12344 9cn 12345 9pos 12358 9m1e8 12379 8p1e9 12395 5p4e9 12403 6p3e9 12405 7p2e9 12406 8lt9 12444 8p2e10 12790 9p9e18 12804 9t9e81 12839 19prm 17090 139prm 17096 bposlem8 27269 lgsdir2lem5 27307 2lgsoddprmlem3d 27391 aks4d1p1 41679 rmydioph 42577 139prmALT 47073 9gbo 47251 wtgoldbnnsum4prm 47279 bgoldbnnsum3prm 47281