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 12279

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 12271	. 2 class 9
2		c8 12270	. . 3 class 8
3		c1 11108	. . 3 class 1
4		caddc 11110	. . 3 class +
5	2, 3, 4	co 7406	. 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 12307 9re 12308 9cn 12309 9pos 12322 9m1e8 12343 8p1e9 12359 5p4e9 12367 6p3e9 12369 7p2e9 12370 8lt9 12408 8p2e10 12754 9p9e18 12768 9t9e81 12803 19prm 17048 139prm 17054 bposlem8 26784 lgsdir2lem5 26822 2lgsoddprmlem3d 26906 aks4d1p1 40930 rmydioph 41739 139prmALT 46251 9gbo 46429 wtgoldbnnsum4prm 46457 bgoldbnnsum3prm 46459