Definition df-7 9046

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 9038	. 2 class 7
2		c6 9037	. . 3 class 6
3		c1 7873	. . 3 class 1
4		caddc 7875	. . 3 class +
5	2, 3, 4	co 5918	. 2 class ( 6 + 1 )
6	1, 5	wceq 1364	1 wff 7 = ( 6 + 1 )

This definition is referenced by:  7re  9065  7pos  9084  7m1e6  9106  6p1e7  9120  4p3e7  9126  5p2e7  9128  6p2e8  9131  7nn  9148  6lt7  9166  7p7e14  9526  8p7e15  9532  9p7e16  9539  9p8e17  9540  7t7e49  9561  8t7e56  9567  9t7e63  9574  lgsdir2lem3  15146