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 12316

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 12308	. 2 class 9
2		c8 12307	. . 3 class 8
3		c1 11107	. . 3 class 1
4		caddc 11109	. . 3 class +
5	2, 3, 4	co 7412	. 2 class (8 + 1)
6	1, 5	wceq 1569	1 wff 9 = (8 + 1)

Colors of variables: wff setvar class

This definition is used by: 9nn 12345 9re 12346 9cn 12347 9m1e8 12380 8p1e9 12396 5p4e9 12404 6p3e9 12406 7p2e9 12407 8lt9 12448 8p2e10 12802 9p9e18 12816 9t9e81 12851 19prm 17184 139prm 17190 bposlem8 27466 lgsdir2lem5 27504 2lgsoddprmlem3d 27588 aks4d1p1 42871 rmydioph 43769 139prmALT 48376 9gbo 48567 wtgoldbnnsum4prm 48595 bgoldbnnsum3prm 48597