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 12052

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 12044	. 2 class 9
2		c8 12043	. . 3 class 8
3		c1 10881	. . 3 class 1
4		caddc 10883	. . 3 class +
5	2, 3, 4	co 7284	. 2 class (8 + 1)
6	1, 5	wceq 1539	1 wff 9 = (8 + 1)

Colors of variables: wff setvar class

This definition is referenced by: 9nn 12080 9re 12081 9cn 12082 9pos 12095 9m1e8 12116 8p1e9 12132 5p4e9 12140 6p3e9 12142 7p2e9 12143 8lt9 12181 8p2e10 12526 9p9e18 12540 9t9e81 12575 19prm 16828 139prm 16834 bposlem8 26448 lgsdir2lem5 26486 2lgsoddprmlem3d 26570 aks4d1p1 40091 rmydioph 40843 139prmALT 45059 9gbo 45237 wtgoldbnnsum4prm 45265 bgoldbnnsum3prm 45267