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 12232

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 12224	. 2 class 9
2		c8 12223	. . 3 class 8
3		c1 11045	. . 3 class 1
4		caddc 11047	. . 3 class +
5	2, 3, 4	co 7369	. 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 12260 9re 12261 9cn 12262 9pos 12275 9m1e8 12291 8p1e9 12307 5p4e9 12315 6p3e9 12317 7p2e9 12318 8lt9 12356 8p2e10 12705 9p9e18 12719 9t9e81 12754 19prm 17064 139prm 17070 bposlem8 27178 lgsdir2lem5 27216 2lgsoddprmlem3d 27300 aks4d1p1 42037 rmydioph 42976 139prmALT 47570 9gbo 47748 wtgoldbnnsum4prm 47776 bgoldbnnsum3prm 47778