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 12381

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 12373	. 2 class 9
2		c8 12372	. . 3 class 8
3		c1 11172	. . 3 class 1
4		caddc 11174	. . 3 class +
5	2, 3, 4	co 7408	. 2 class (8 + 1)
6	1, 5	wceq 1570	1 wff 9 = (8 + 1)

Colors of variables: wff setvar class

This definition is used by: 9nn 12410 9re 12411 9cn 12412 9m1e8 12445 8p1e9 12461 5p4e9 12469 6p3e9 12471 7p2e9 12472 8lt9 12513 8p2e10 12868 9p9e18 12882 9t9e81 12917 19prm 17257 139prm 17263 bposlem8 27581 lgsdir2lem5 27619 2lgsoddprmlem3d 27703 aks4d1p1 43046 rmydioph 43959 139prmALT 48603 9gbo 48794 wtgoldbnnsum4prm 48822 bgoldbnnsum3prm 48824