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 11708

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 11700	. 2 class 9
2		c8 11699	. . 3 class 8
3		c1 10538	. . 3 class 1
4		caddc 10540	. . 3 class +
5	2, 3, 4	co 7156	. 2 class (8 + 1)
6	1, 5	wceq 1537	1 wff 9 = (8 + 1)

Colors of variables: wff setvar class

This definition is referenced by: 9nn 11736 9re 11737 9cn 11738 9pos 11751 9m1e8 11772 8p1e9 11788 5p4e9 11796 6p3e9 11798 7p2e9 11799 8lt9 11837 8p2e10 12179 9p9e18 12193 9t9e81 12228 19prm 16451 139prm 16457 bposlem8 25867 lgsdir2lem5 25905 2lgsoddprmlem3d 25989 rmydioph 39660 139prmALT 43808 9gbo 43988 wtgoldbnnsum4prm 44016 bgoldbnnsum3prm 44018