Definition df-7 8784

Description: Define the number 7. (Contributed by NM, 27-May-1999.)

Assertion

Ref	Expression
df-7	|- 7 = ( 6 + 1 )

Detailed syntax breakdown of Definition df-7

Step	Hyp	Ref	Expression
1		c7 8776	. 2 class 7
2		c6 8775	. . 3 class 6
3		c1 7621	. . 3 class 1
4		caddc 7623	. . 3 class +
5	2, 3, 4	co 5774	. 2 class ( 6 + 1 )
6	1, 5	wceq 1331	1 wff 7 = ( 6 + 1 )

This definition is referenced by:  7re  8803  7pos  8822  7m1e6  8844  6p1e7  8858  4p3e7  8864  5p2e7  8866  6p2e8  8869  7nn  8886  6lt7  8904  7p7e14  9260  8p7e15  9266  9p7e16  9273  9p8e17  9274  7t7e49  9295  8t7e56  9301  9t7e63  9308