Definition df-7 9347

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 9339	. 2 class 7
2		c6 9338	. . 3 class 6
3		c1 8170	. . 3 class 1
4		caddc 8172	. . 3 class +
5	2, 3, 4	co 6075	. 2 class (6 + 1)
6	1, 5	wceq 1402	1 wff 7 = (6 + 1)

This definition is referenced by:  7re  9366  7pos  9385  7m1e6  9407  6p1e7  9422  4p3e7  9428  5p2e7  9430  6p2e8  9433  7nn  9450  6lt7  9468  7p7e14  9834  8p7e15  9840  9p7e16  9847  9p8e17  9848  7t7e49  9869  8t7e56  9875  9t7e63  9882  2exp7  13191  lgsdir2lem3  16063