Definition df-7 9303

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 9295	. 2 class 7
2		c6 9294	. . 3 class 6
3		c1 8130	. . 3 class 1
4		caddc 8132	. . 3 class +
5	2, 3, 4	co 6052	. 2 class ( 6 + 1 )
6	1, 5	wceq 1398	1 wff 7 = ( 6 + 1 )

This definition is referenced by:  7re  9322  7pos  9341  7m1e6  9363  6p1e7  9378  4p3e7  9384  5p2e7  9386  6p2e8  9389  7nn  9406  6lt7  9424  7p7e14  9790  8p7e15  9796  9p7e16  9803  9p8e17  9804  7t7e49  9825  8t7e56  9831  9t7e63  9838  2exp7  13136  lgsdir2lem3  15920