Definition df-7 9073

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 9065	. 2 class 7
2		c6 9064	. . 3 class 6
3		c1 7899	. . 3 class 1
4		caddc 7901	. . 3 class +
5	2, 3, 4	co 5925	. 2 class (6 + 1)
6	1, 5	wceq 1364	1 wff 7 = (6 + 1)

This definition is referenced by:  7re  9092  7pos  9111  7m1e6  9133  6p1e7  9148  4p3e7  9154  5p2e7  9156  6p2e8  9159  7nn  9176  6lt7  9194  7p7e14  9554  8p7e15  9560  9p7e16  9567  9p8e17  9568  7t7e49  9589  8t7e56  9595  9t7e63  9602  2exp7  12630  lgsdir2lem3  15379