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 12219

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 12211	. 2 class 9
2		c8 12210	. . 3 class 8
3		c1 11031	. . 3 class 1
4		caddc 11033	. . 3 class +
5	2, 3, 4	co 7360	. 2 class (8 + 1)
6	1, 5	wceq 1542	1 wff 9 = (8 + 1)

Colors of variables: wff setvar class

This definition is referenced by: 9nn 12247 9re 12248 9cn 12249 9pos 12262 9m1e8 12278 8p1e9 12294 5p4e9 12302 6p3e9 12304 7p2e9 12305 8lt9 12343 8p2e10 12691 9p9e18 12705 9t9e81 12740 19prm 17049 139prm 17055 bposlem8 27262 lgsdir2lem5 27300 2lgsoddprmlem3d 27384 aks4d1p1 42398 rmydioph 43323 139prmALT 47909 9gbo 48087 wtgoldbnnsum4prm 48115 bgoldbnnsum3prm 48117