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 12436

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 12428	. 2 class 9
2		c8 12427	. . 3 class 8
3		c1 11225	. . 3 class 1
4		caddc 11227	. . 3 class +
5	2, 3, 4	co 7440	. 2 class (8 + 1)
6	1, 5	wceq 1570	1 wff 9 = (8 + 1)

Colors of variables: wff setvar class

This definition is used by: 9nn 12465 9re 12466 9cn 12467 9m1e8 12500 8p1e9 12516 5p4e9 12524 6p3e9 12526 7p2e9 12527 8lt9 12568 8p2e10 12923 9p9e18 12937 9t9e81 12972 19prm 17322 139prm 17328 bposlem8 27645 lgsdir2lem5 27683 2lgsoddprmlem3d 27767 aks4d1p1 43317 rmydioph 44212 139prmALT 48884 9gbo 49075 wtgoldbnnsum4prm 49103 bgoldbnnsum3prm 49105