Definition df-7 9048

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 9040	. 2 class 7
2		c6 9039	. . 3 class 6
3		c1 7875	. . 3 class 1
4		caddc 7877	. . 3 class +
5	2, 3, 4	co 5919	. 2 class ( 6 + 1 )
6	1, 5	wceq 1364	1 wff 7 = ( 6 + 1 )

This definition is referenced by:  7re  9067  7pos  9086  7m1e6  9108  6p1e7  9123  4p3e7  9129  5p2e7  9131  6p2e8  9134  7nn  9151  6lt7  9169  7p7e14  9529  8p7e15  9535  9p7e16  9542  9p8e17  9543  7t7e49  9564  8t7e56  9570  9t7e63  9577  lgsdir2lem3  15187