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 12412

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 12404	. 2 class 9
2		c8 12403	. . 3 class 8
3		c1 11201	. . 3 class 1
4		caddc 11203	. . 3 class +
5	2, 3, 4	co 7420	. 2 class (8 + 1)
6	1, 5	wceq 1569	1 wff 9 = (8 + 1)

Colors of variables: wff setvar class

This definition is used by: 9nn 12441 9re 12442 9cn 12443 9m1e8 12476 8p1e9 12492 5p4e9 12500 6p3e9 12502 7p2e9 12503 8lt9 12544 8p2e10 12899 9p9e18 12913 9t9e81 12948 19prm 17296 139prm 17302 bposlem8 27618 lgsdir2lem5 27656 2lgsoddprmlem3d 27740 aks4d1p1 43127 rmydioph 44021 139prmALT 48681 9gbo 48872 wtgoldbnnsum4prm 48900 bgoldbnnsum3prm 48902