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  9871  9p9e18  9885  9t9e81  9920  19prm  13260  139prm  13266  bposlem8  16335  lgsdir2lem5  16373  2lgsoddprmlem3d  16451