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 11504

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 11496	. 2 class 9
2		c8 11495	. . 3 class 8
3		c1 10330	. . 3 class 1
4		caddc 10332	. . 3 class +
5	2, 3, 4	co 6970	. 2 class (8 + 1)
6	1, 5	wceq 1507	1 wff 9 = (8 + 1)

Colors of variables: wff setvar class

This definition is referenced by: 9nn 11538 9re 11539 9cn 11540 9pos 11554 9m1e8 11575 8p1e9 11591 5p4e9 11599 6p3e9 11601 7p2e9 11602 8lt9 11640 8p2e10 11987 9p9e18 12001 9t9e81 12036 19prm 16301 139prm 16307 bposlem8 25563 lgsdir2lem5 25601 2lgsoddprmlem3d 25685 rmydioph 39007 139prmALT 43127 9gbo 43307 wtgoldbnnsum4prm 43335 bgoldbnnsum3prm 43337