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 12363

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 12355	. 2 class 9
2		c8 12354	. . 3 class 8
3		c1 11185	. . 3 class 1
4		caddc 11187	. . 3 class +
5	2, 3, 4	co 7448	. 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 12391 9re 12392 9cn 12393 9pos 12406 9m1e8 12427 8p1e9 12443 5p4e9 12451 6p3e9 12453 7p2e9 12454 8lt9 12492 8p2e10 12838 9p9e18 12852 9t9e81 12887 19prm 17165 139prm 17171 bposlem8 27353 lgsdir2lem5 27391 2lgsoddprmlem3d 27475 aks4d1p1 42033 rmydioph 42971 139prmALT 47470 9gbo 47648 wtgoldbnnsum4prm 47676 bgoldbnnsum3prm 47678