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 12308

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 12300	. 2 class 9
2		c8 12299	. . 3 class 8
3		c1 11128	. . 3 class 1
4		caddc 11130	. . 3 class +
5	2, 3, 4	co 7403	. 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 12336 9re 12337 9cn 12338 9pos 12351 9m1e8 12372 8p1e9 12388 5p4e9 12396 6p3e9 12398 7p2e9 12399 8lt9 12437 8p2e10 12786 9p9e18 12800 9t9e81 12835 19prm 17135 139prm 17141 bposlem8 27252 lgsdir2lem5 27290 2lgsoddprmlem3d 27374 aks4d1p1 42035 rmydioph 42985 139prmALT 47558 9gbo 47736 wtgoldbnnsum4prm 47764 bgoldbnnsum3prm 47766