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 12213

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 12205	. 2 class 9
2		c8 12204	. . 3 class 8
3		c1 11025	. . 3 class 1
4		caddc 11027	. . 3 class +
5	2, 3, 4	co 7356	. 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 12241 9re 12242 9cn 12243 9pos 12256 9m1e8 12272 8p1e9 12288 5p4e9 12296 6p3e9 12298 7p2e9 12299 8lt9 12337 8p2e10 12685 9p9e18 12699 9t9e81 12734 19prm 17043 139prm 17049 bposlem8 27256 lgsdir2lem5 27294 2lgsoddprmlem3d 27378 aks4d1p1 42269 rmydioph 43198 139prmALT 47784 9gbo 47962 wtgoldbnnsum4prm 47990 bgoldbnnsum3prm 47992