Definition df-7 8983

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 8975	. 2 class 7
2		c6 8974	. . 3 class 6
3		c1 7812	. . 3 class 1
4		caddc 7814	. . 3 class +
5	2, 3, 4	co 5875	. 2 class ( 6 + 1 )
6	1, 5	wceq 1353	1 wff 7 = ( 6 + 1 )

This definition is referenced by:  7re  9002  7pos  9021  7m1e6  9043  6p1e7  9057  4p3e7  9063  5p2e7  9065  6p2e8  9068  7nn  9085  6lt7  9103  7p7e14  9462  8p7e15  9468  9p7e16  9475  9p8e17  9476  7t7e49  9497  8t7e56  9503  9t7e63  9510  lgsdir2lem3  14434