Definition df-9 9372

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 9364	. 2 class 9
2		c8 9363	. . 3 class 8
3		c1 8180	. . 3 class 1
4		caddc 8182	. . 3 class +
5	2, 3, 4	co 6085	. 2 class ( 8 + 1 )
6	1, 5	wceq 1402	1 wff 9 = ( 8 + 1 )

This definition is used by:  9re  9393  9pos  9410  9m1e8  9432  8p1e9  9447  5p4e9  9455  6p3e9  9457  7p2e9  9458  9nn  9477  8lt9  9506  8p2e10  9865  9p9e18  9879  9t9e81  9914  19prm  13252  139prm  13258  lgsdir2lem5  16249  2lgsoddprmlem3d  16327