Definition df-7 8942

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 8934	. 2 class 7
2		c6 8933	. . 3 class 6
3		c1 7775	. . 3 class 1
4		caddc 7777	. . 3 class +
5	2, 3, 4	co 5853	. 2 class ( 6 + 1 )
6	1, 5	wceq 1348	1 wff 7 = ( 6 + 1 )

This definition is referenced by:  7re  8961  7pos  8980  7m1e6  9002  6p1e7  9016  4p3e7  9022  5p2e7  9024  6p2e8  9027  7nn  9044  6lt7  9062  7p7e14  9421  8p7e15  9427  9p7e16  9434  9p8e17  9435  7t7e49  9456  8t7e56  9462  9t7e63  9469  lgsdir2lem3  13725