Definition df-7 9350

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 9342	. 2 class 7
2		c6 9341	. . 3 class 6
3		c1 8173	. . 3 class 1
4		caddc 8175	. . 3 class +
5	2, 3, 4	co 6078	. 2 class ( 6 + 1 )
6	1, 5	wceq 1402	1 wff 7 = ( 6 + 1 )

This definition is referenced by:  7re  9369  7pos  9388  7m1e6  9410  6p1e7  9425  4p3e7  9431  5p2e7  9433  6p2e8  9436  7nn  9453  6lt7  9471  7p7e14  9837  8p7e15  9843  9p7e16  9850  9p8e17  9851  7t7e49  9872  8t7e56  9878  9t7e63  9885  2exp7  13194  lgsdir2lem3  16066