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 12195

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 12187	. 2 class 9
2		c8 12186	. . 3 class 8
3		c1 11007	. . 3 class 1
4		caddc 11009	. . 3 class +
5	2, 3, 4	co 7346	. 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 12223 9re 12224 9cn 12225 9pos 12238 9m1e8 12254 8p1e9 12270 5p4e9 12278 6p3e9 12280 7p2e9 12281 8lt9 12319 8p2e10 12668 9p9e18 12682 9t9e81 12717 19prm 17029 139prm 17035 bposlem8 27229 lgsdir2lem5 27267 2lgsoddprmlem3d 27351 aks4d1p1 42179 rmydioph 43117 139prmALT 47706 9gbo 47884 wtgoldbnnsum4prm 47912 bgoldbnnsum3prm 47914