Definition df-9 9373

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 9365	. 2 class 9
2		c8 9364	. . 3 class 8
3		c1 8181	. . 3 class 1
4		caddc 8183	. . 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  9394  9pos  9411  9m1e8  9433  8p1e9  9448  5p4e9  9456  6p3e9  9458  7p2e9  9459  9nn  9478  8lt9  9507  8p2e10  9866  9p9e18  9880  9t9e81  9915  19prm  13255  139prm  13261  bposlem8  16279  lgsdir2lem5  16317  2lgsoddprmlem3d  16395