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 12309

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 12301	. 2 class 9
2		c8 12300	. . 3 class 8
3		c1 11100	. . 3 class 1
4		caddc 11102	. . 3 class +
5	2, 3, 4	co 7410	. 2 class (8 + 1)
6	1, 5	wceq 1568	1 wff 9 = (8 + 1)

Colors of variables: wff setvar class

This definition is referenced by: 9nn 12338 9re 12339 9cn 12340 9m1e8 12373 8p1e9 12389 5p4e9 12397 6p3e9 12399 7p2e9 12400 8lt9 12441 8p2e10 12795 9p9e18 12809 9t9e81 12844 19prm 17177 139prm 17183 bposlem8 27431 lgsdir2lem5 27469 2lgsoddprmlem3d 27553 aks4d1p1 42789 rmydioph 43689 139prmALT 48293 9gbo 48484 wtgoldbnnsum4prm 48512 bgoldbnnsum3prm 48514