Definition df-7 9174

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 9166	. 2 class 7
2		c6 9165	. . 3 class 6
3		c1 8000	. . 3 class 1
4		caddc 8002	. . 3 class +
5	2, 3, 4	co 6001	. 2 class ( 6 + 1 )
6	1, 5	wceq 1395	1 wff 7 = ( 6 + 1 )

This definition is referenced by:  7re  9193  7pos  9212  7m1e6  9234  6p1e7  9249  4p3e7  9255  5p2e7  9257  6p2e8  9260  7nn  9277  6lt7  9295  7p7e14  9656  8p7e15  9662  9p7e16  9669  9p8e17  9670  7t7e49  9691  8t7e56  9697  9t7e63  9704  2exp7  12957  lgsdir2lem3  15709