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 12289

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 12281	. 2 class 9
2		c8 12280	. . 3 class 8
3		c1 11076	. . 3 class 1
4		caddc 11078	. . 3 class +
5	2, 3, 4	co 7398	. 2 class (8 + 1)
6	1, 5	wceq 1562	1 wff 9 = (8 + 1)

Colors of variables: wff setvar class

This definition is referenced by: 9nn 12318 9re 12319 9cn 12320 9m1e8 12353 8p1e9 12369 5p4e9 12377 6p3e9 12379 7p2e9 12380 8lt9 12421 8p2e10 12775 9p9e18 12789 9t9e81 12824 19prm 17156 139prm 17162 bposlem8 27357 lgsdir2lem5 27395 2lgsoddprmlem3d 27479 aks4d1p1 42698 rmydioph 43596 139prmALT 48210 9gbo 48401 wtgoldbnnsum4prm 48429 bgoldbnnsum3prm 48431