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 11865

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 11857	. 2 class 9
2		c8 11856	. . 3 class 8
3		c1 10695	. . 3 class 1
4		caddc 10697	. . 3 class +
5	2, 3, 4	co 7191	. 2 class (8 + 1)
6	1, 5	wceq 1543	1 wff 9 = (8 + 1)

Colors of variables: wff setvar class

This definition is referenced by: 9nn 11893 9re 11894 9cn 11895 9pos 11908 9m1e8 11929 8p1e9 11945 5p4e9 11953 6p3e9 11955 7p2e9 11956 8lt9 11994 8p2e10 12338 9p9e18 12352 9t9e81 12387 19prm 16634 139prm 16640 bposlem8 26126 lgsdir2lem5 26164 2lgsoddprmlem3d 26248 aks4d1p1 39766 rmydioph 40480 139prmALT 44664 9gbo 44842 wtgoldbnnsum4prm 44870 bgoldbnnsum3prm 44872