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 12229

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 12221	. 2 class 9
2		c8 12220	. . 3 class 8
3		c1 11041	. . 3 class 1
4		caddc 11043	. . 3 class +
5	2, 3, 4	co 7370	. 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 12257 9re 12258 9cn 12259 9pos 12272 9m1e8 12288 8p1e9 12304 5p4e9 12312 6p3e9 12314 7p2e9 12315 8lt9 12353 8p2e10 12701 9p9e18 12715 9t9e81 12750 19prm 17059 139prm 17065 bposlem8 27275 lgsdir2lem5 27313 2lgsoddprmlem3d 27397 aks4d1p1 42475 rmydioph 43400 139prmALT 47985 9gbo 48163 wtgoldbnnsum4prm 48191 bgoldbnnsum3prm 48193