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 12149

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 12141	. 2 class 9
2		c8 12140	. . 3 class 8
3		c1 10978	. . 3 class 1
4		caddc 10980	. . 3 class +
5	2, 3, 4	co 7342	. 2 class (8 + 1)
6	1, 5	wceq 1541	1 wff 9 = (8 + 1)

Colors of variables: wff setvar class

This definition is referenced by: 9nn 12177 9re 12178 9cn 12179 9pos 12192 9m1e8 12213 8p1e9 12229 5p4e9 12237 6p3e9 12239 7p2e9 12240 8lt9 12278 8p2e10 12623 9p9e18 12637 9t9e81 12672 19prm 16917 139prm 16923 bposlem8 26545 lgsdir2lem5 26583 2lgsoddprmlem3d 26667 aks4d1p1 40387 rmydioph 41148 139prmALT 45464 9gbo 45642 wtgoldbnnsum4prm 45670 bgoldbnnsum3prm 45672