Definition df-9 11086

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 11077	. 2 class 9
2		c8 11076	. . 3 class 8
3		c1 9937	. . 3 class 1
4		caddc 9939	. . 3 class +
5	2, 3, 4	co 6650	. 2 class ( 8 + 1 )
6	1, 5	wceq 1483	1 wff 9 = ( 8 + 1 )

This definition is referenced by:  9re  11107  9pos  11122  9m1e8  11143  8p1e9  11158  5p4e9  11167  6p3e9  11170  7p2e9  11172  8p2e10OLD  11174  9nn  11192  8lt9  11222  8p2e10  11610  9p9e18  11627  9t9e81  11670  19prm  15825  139prm  15831  log2tlbnd  24672  bposlem8  25016  lgsdir2lem5  25054  2lgsoddprmlem3b  25136  2lgsoddprmlem3d  25138  rmydioph  37581  139prmALT  41511  9gbo  41662  wtgoldbnnsum4prm  41690  bgoldbnnsum3prm  41692