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 12246

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 12238	. 2 class 9
2		c8 12237	. . 3 class 8
3		c1 11035	. . 3 class 1
4		caddc 11037	. . 3 class +
5	2, 3, 4	co 7359	. 2 class (8 + 1)
6	1, 5	wceq 1548	1 wff 9 = (8 + 1)

Colors of variables: wff setvar class

This definition is referenced by: 9nn 12274 9re 12275 9cn 12276 9pos 12289 9m1e8 12305 8p1e9 12321 5p4e9 12329 6p3e9 12331 7p2e9 12332 8lt9 12370 8p2e10 12719 9p9e18 12733 9t9e81 12768 19prm 17083 139prm 17089 bposlem8 27275 lgsdir2lem5 27313 2lgsoddprmlem3d 27397 aks4d1p1 42574 rmydioph 43472 139prmALT 48086 9gbo 48277 wtgoldbnnsum4prm 48305 bgoldbnnsum3prm 48307