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 12240

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 12232	. 2 class 9
2		c8 12231	. . 3 class 8
3		c1 11028	. . 3 class 1
4		caddc 11030	. . 3 class +
5	2, 3, 4	co 7356	. 2 class (8 + 1)
6	1, 5	wceq 1542	1 wff 9 = (8 + 1)

Colors of variables: wff setvar class

This definition is referenced by: 9nn 12268 9re 12269 9cn 12270 9pos 12283 9m1e8 12299 8p1e9 12315 5p4e9 12323 6p3e9 12325 7p2e9 12326 8lt9 12364 8p2e10 12713 9p9e18 12727 9t9e81 12762 19prm 17077 139prm 17083 bposlem8 27242 lgsdir2lem5 27280 2lgsoddprmlem3d 27364 aks4d1p1 42503 rmydioph 43430 139prmALT 48047 9gbo 48238 wtgoldbnnsum4prm 48266 bgoldbnnsum3prm 48268