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 12248

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 12240	. 2 class 9
2		c8 12239	. . 3 class 8
3		c1 11036	. . 3 class 1
4		caddc 11038	. . 3 class +
5	2, 3, 4	co 7364	. 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 12276 9re 12277 9cn 12278 9pos 12291 9m1e8 12307 8p1e9 12323 5p4e9 12331 6p3e9 12333 7p2e9 12334 8lt9 12372 8p2e10 12721 9p9e18 12735 9t9e81 12770 19prm 17085 139prm 17091 bposlem8 27251 lgsdir2lem5 27289 2lgsoddprmlem3d 27373 aks4d1p1 42512 rmydioph 43439 139prmALT 48050 9gbo 48241 wtgoldbnnsum4prm 48269 bgoldbnnsum3prm 48271