Definition df-7 9099

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 9091	. 2 class 7
2		c6 9090	. . 3 class 6
3		c1 7925	. . 3 class 1
4		caddc 7927	. . 3 class +
5	2, 3, 4	co 5943	. 2 class (6 + 1)
6	1, 5	wceq 1372	1 wff 7 = (6 + 1)

This definition is referenced by:  7re  9118  7pos  9137  7m1e6  9159  6p1e7  9174  4p3e7  9180  5p2e7  9182  6p2e8  9185  7nn  9202  6lt7  9220  7p7e14  9581  8p7e15  9587  9p7e16  9594  9p8e17  9595  7t7e49  9616  8t7e56  9622  9t7e63  9629  2exp7  12699  lgsdir2lem3  15449