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 12333

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 12325	. 2 class 9
2		c8 12324	. . 3 class 8
3		c1 11153	. . 3 class 1
4		caddc 11155	. . 3 class +
5	2, 3, 4	co 7430	. 2 class (8 + 1)
6	1, 5	wceq 1536	1 wff 9 = (8 + 1)

Colors of variables: wff setvar class

This definition is referenced by: 9nn 12361 9re 12362 9cn 12363 9pos 12376 9m1e8 12397 8p1e9 12413 5p4e9 12421 6p3e9 12423 7p2e9 12424 8lt9 12462 8p2e10 12810 9p9e18 12824 9t9e81 12859 19prm 17151 139prm 17157 bposlem8 27349 lgsdir2lem5 27387 2lgsoddprmlem3d 27471 aks4d1p1 42057 rmydioph 43002 139prmALT 47520 9gbo 47698 wtgoldbnnsum4prm 47726 bgoldbnnsum3prm 47728