Definition df-9 9379

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 9371	. 2 class 9
2		c8 9370	. . 3 class 8
3		c1 8186	. . 3 class 1
4		caddc 8188	. . 3 class +
5	2, 3, 4	co 6088	. 2 class ( 8 + 1 )
6	1, 5	wceq 1402	1 wff 9 = ( 8 + 1 )

This definition is used by:  9re  9400  9pos  9417  9m1e8  9439  8p1e9  9454  5p4e9  9462  6p3e9  9464  7p2e9  9465  9nn  9484  8lt9  9513  8p2e10  9872  9p9e18  9886  9t9e81  9921  19prm  13261  139prm  13267  bposlem8  16318  lgsdir2lem5  16356  2lgsoddprmlem3d  16434