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 12251

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 12243	. 2 class 9
2		c8 12242	. . 3 class 8
3		c1 11039	. . 3 class 1
4		caddc 11041	. . 3 class +
5	2, 3, 4	co 7367	. 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 12279 9re 12280 9cn 12281 9pos 12294 9m1e8 12310 8p1e9 12326 5p4e9 12334 6p3e9 12336 7p2e9 12337 8lt9 12375 8p2e10 12724 9p9e18 12738 9t9e81 12773 19prm 17088 139prm 17094 bposlem8 27254 lgsdir2lem5 27292 2lgsoddprmlem3d 27376 aks4d1p1 42515 rmydioph 43442 139prmALT 48053 9gbo 48244 wtgoldbnnsum4prm 48272 bgoldbnnsum3prm 48274