Definition df-7 8921

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 8913	. 2 class 7
2		c6 8912	. . 3 class 6
3		c1 7754	. . 3 class 1
4		caddc 7756	. . 3 class +
5	2, 3, 4	co 5842	. 2 class ( 6 + 1 )
6	1, 5	wceq 1343	1 wff 7 = ( 6 + 1 )

This definition is referenced by:  7re  8940  7pos  8959  7m1e6  8981  6p1e7  8995  4p3e7  9001  5p2e7  9003  6p2e8  9006  7nn  9023  6lt7  9041  7p7e14  9400  8p7e15  9406  9p7e16  9413  9p8e17  9414  7t7e49  9435  8t7e56  9441  9t7e63  9448  lgsdir2lem3  13571