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 12198

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 12190	. 2 class 9
2		c8 12189	. . 3 class 8
3		c1 11010	. . 3 class 1
4		caddc 11012	. . 3 class +
5	2, 3, 4	co 7349	. 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 12226 9re 12227 9cn 12228 9pos 12241 9m1e8 12257 8p1e9 12273 5p4e9 12281 6p3e9 12283 7p2e9 12284 8lt9 12322 8p2e10 12671 9p9e18 12685 9t9e81 12720 19prm 17029 139prm 17035 bposlem8 27200 lgsdir2lem5 27238 2lgsoddprmlem3d 27322 aks4d1p1 42053 rmydioph 42991 139prmALT 47584 9gbo 47762 wtgoldbnnsum4prm 47790 bgoldbnnsum3prm 47792