Definition df-7 8777

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 8769	. 2 class 7
2		c6 8768	. . 3 class 6
3		c1 7614	. . 3 class 1
4		caddc 7616	. . 3 class +
5	2, 3, 4	co 5767	. 2 class ( 6 + 1 )
6	1, 5	wceq 1331	1 wff 7 = ( 6 + 1 )

This definition is referenced by:  7re  8796  7pos  8815  7m1e6  8837  6p1e7  8851  4p3e7  8857  5p2e7  8859  6p2e8  8862  7nn  8879  6lt7  8897  7p7e14  9253  8p7e15  9259  9p7e16  9266  9p8e17  9267  7t7e49  9288  8t7e56  9294  9t7e63  9301