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 12337

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 12329	. 2 class 9
2		c8 12328	. . 3 class 8
3		c1 11128	. . 3 class 1
4		caddc 11130	. . 3 class +
5	2, 3, 4	co 7416	. 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 12366 9re 12367 9cn 12368 9m1e8 12401 8p1e9 12417 5p4e9 12425 6p3e9 12427 7p2e9 12428 8lt9 12469 8p2e10 12824 9p9e18 12838 9t9e81 12873 19prm 17214 139prm 17220 bposlem8 27525 lgsdir2lem5 27563 2lgsoddprmlem3d 27647 aks4d1p1 42929 rmydioph 43842 139prmALT 48486 9gbo 48677 wtgoldbnnsum4prm 48705 bgoldbnnsum3prm 48707