Definition df-7 9206

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 9198	. 2 class 7
2		c6 9197	. . 3 class 6
3		c1 8032	. . 3 class 1
4		caddc 8034	. . 3 class +
5	2, 3, 4	co 6017	. 2 class (6 + 1)
6	1, 5	wceq 1397	1 wff 7 = (6 + 1)

This definition is referenced by:  7re  9225  7pos  9244  7m1e6  9266  6p1e7  9281  4p3e7  9287  5p2e7  9289  6p2e8  9292  7nn  9309  6lt7  9327  7p7e14  9688  8p7e15  9694  9p7e16  9701  9p8e17  9702  7t7e49  9723  8t7e56  9729  9t7e63  9736  2exp7  13006  lgsdir2lem3  15758