Definition df-7 9195

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 9187	. 2 class 7
2		c6 9186	. . 3 class 6
3		c1 8021	. . 3 class 1
4		caddc 8023	. . 3 class +
5	2, 3, 4	co 6011	. 2 class (6 + 1)
6	1, 5	wceq 1395	1 wff 7 = (6 + 1)

This definition is referenced by:  7re  9214  7pos  9233  7m1e6  9255  6p1e7  9270  4p3e7  9276  5p2e7  9278  6p2e8  9281  7nn  9298  6lt7  9316  7p7e14  9677  8p7e15  9683  9p7e16  9690  9p8e17  9691  7t7e49  9712  8t7e56  9718  9t7e63  9725  2exp7  12994  lgsdir2lem3  15746