Definition df-7 9301

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 9293	. 2 class 7
2		c6 9292	. . 3 class 6
3		c1 8128	. . 3 class 1
4		caddc 8130	. . 3 class +
5	2, 3, 4	co 6050	. 2 class (6 + 1)
6	1, 5	wceq 1398	1 wff 7 = (6 + 1)

This definition is referenced by:  7re  9320  7pos  9339  7m1e6  9361  6p1e7  9376  4p3e7  9382  5p2e7  9384  6p2e8  9387  7nn  9404  6lt7  9422  7p7e14  9787  8p7e15  9793  9p7e16  9800  9p8e17  9801  7t7e49  9822  8t7e56  9828  9t7e63  9835  2exp7  13132  lgsdir2lem3  15903