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 12263

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 12255	. 2 class 9
2		c8 12254	. . 3 class 8
3		c1 11076	. . 3 class 1
4		caddc 11078	. . 3 class +
5	2, 3, 4	co 7390	. 2 class (8 + 1)
6	1, 5	wceq 1540	1 wff 9 = (8 + 1)

Colors of variables: wff setvar class

This definition is referenced by: 9nn 12291 9re 12292 9cn 12293 9pos 12306 9m1e8 12322 8p1e9 12338 5p4e9 12346 6p3e9 12348 7p2e9 12349 8lt9 12387 8p2e10 12736 9p9e18 12750 9t9e81 12785 19prm 17095 139prm 17101 bposlem8 27209 lgsdir2lem5 27247 2lgsoddprmlem3d 27331 aks4d1p1 42071 rmydioph 43010 139prmALT 47601 9gbo 47779 wtgoldbnnsum4prm 47807 bgoldbnnsum3prm 47809