Definition df-7 9249

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 9241	. 2 class 7
2		c6 9240	. . 3 class 6
3		c1 8076	. . 3 class 1
4		caddc 8078	. . 3 class +
5	2, 3, 4	co 6028	. 2 class (6 + 1)
6	1, 5	wceq 1398	1 wff 7 = (6 + 1)

This definition is referenced by:  7re  9268  7pos  9287  7m1e6  9309  6p1e7  9324  4p3e7  9330  5p2e7  9332  6p2e8  9335  7nn  9352  6lt7  9370  7p7e14  9733  8p7e15  9739  9p7e16  9746  9p8e17  9747  7t7e49  9768  8t7e56  9774  9t7e63  9781  2exp7  13070  lgsdir2lem3  15832