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 11973

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 11965	. 2 class 9
2		c8 11964	. . 3 class 8
3		c1 10803	. . 3 class 1
4		caddc 10805	. . 3 class +
5	2, 3, 4	co 7255	. 2 class (8 + 1)
6	1, 5	wceq 1539	1 wff 9 = (8 + 1)

Colors of variables: wff setvar class

This definition is referenced by: 9nn 12001 9re 12002 9cn 12003 9pos 12016 9m1e8 12037 8p1e9 12053 5p4e9 12061 6p3e9 12063 7p2e9 12064 8lt9 12102 8p2e10 12446 9p9e18 12460 9t9e81 12495 19prm 16747 139prm 16753 bposlem8 26344 lgsdir2lem5 26382 2lgsoddprmlem3d 26466 aks4d1p1 40012 rmydioph 40752 139prmALT 44936 9gbo 45114 wtgoldbnnsum4prm 45142 bgoldbnnsum3prm 45144