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 12282

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 12274	. 2 class 9
2		c8 12273	. . 3 class 8
3		c1 11111	. . 3 class 1
4		caddc 11113	. . 3 class +
5	2, 3, 4	co 7409	. 2 class (8 + 1)
6	1, 5	wceq 1542	1 wff 9 = (8 + 1)

Colors of variables: wff setvar class

This definition is referenced by: 9nn 12310 9re 12311 9cn 12312 9pos 12325 9m1e8 12346 8p1e9 12362 5p4e9 12370 6p3e9 12372 7p2e9 12373 8lt9 12411 8p2e10 12757 9p9e18 12771 9t9e81 12806 19prm 17051 139prm 17057 bposlem8 26794 lgsdir2lem5 26832 2lgsoddprmlem3d 26916 aks4d1p1 40941 rmydioph 41753 139prmALT 46264 9gbo 46442 wtgoldbnnsum4prm 46470 bgoldbnnsum3prm 46472