Definition df-7 9120

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 9112	. 2 class 7
2		c6 9111	. . 3 class 6
3		c1 7946	. . 3 class 1
4		caddc 7948	. . 3 class +
5	2, 3, 4	co 5957	. 2 class (6 + 1)
6	1, 5	wceq 1373	1 wff 7 = (6 + 1)

This definition is referenced by:  7re  9139  7pos  9158  7m1e6  9180  6p1e7  9195  4p3e7  9201  5p2e7  9203  6p2e8  9206  7nn  9223  6lt7  9241  7p7e14  9602  8p7e15  9608  9p7e16  9615  9p8e17  9616  7t7e49  9637  8t7e56  9643  9t7e63  9650  2exp7  12832  lgsdir2lem3  15582