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 12336

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 12328	. 2 class 9
2		c8 12327	. . 3 class 8
3		c1 11156	. . 3 class 1
4		caddc 11158	. . 3 class +
5	2, 3, 4	co 7431	. 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 12364 9re 12365 9cn 12366 9pos 12379 9m1e8 12400 8p1e9 12416 5p4e9 12424 6p3e9 12426 7p2e9 12427 8lt9 12465 8p2e10 12813 9p9e18 12827 9t9e81 12862 19prm 17155 139prm 17161 bposlem8 27335 lgsdir2lem5 27373 2lgsoddprmlem3d 27457 aks4d1p1 42077 rmydioph 43026 139prmALT 47583 9gbo 47761 wtgoldbnnsum4prm 47789 bgoldbnnsum3prm 47791