Definition df-7 9266

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 9258	. 2 class 7
2		c6 9257	. . 3 class 6
3		c1 8093	. . 3 class 1
4		caddc 8095	. . 3 class +
5	2, 3, 4	co 6028	. 2 class ( 6 + 1 )
6	1, 5	wceq 1398	1 wff 7 = ( 6 + 1 )

This definition is referenced by:  7re  9285  7pos  9304  7m1e6  9326  6p1e7  9341  4p3e7  9347  5p2e7  9349  6p2e8  9352  7nn  9369  6lt7  9387  7p7e14  9750  8p7e15  9756  9p7e16  9763  9p8e17  9764  7t7e49  9785  8t7e56  9791  9t7e63  9798  2exp7  13087  lgsdir2lem3  15849