Definition df-7 9368

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 9360	. 2 class 7
2		c6 9359	. . 3 class 6
3		c1 8180	. . 3 class 1
4		caddc 8182	. . 3 class +
5	2, 3, 4	co 6085	. 2 class ( 6 + 1 )
6	1, 5	wceq 1402	1 wff 7 = ( 6 + 1 )

This definition is used by:  7re  9387  7pos  9406  7m1e6  9428  6p1e7  9443  4p3e7  9449  5p2e7  9451  6p2e8  9454  7nn  9471  6lt7  9489  7p7e14  9855  8p7e15  9861  9p7e16  9868  9p8e17  9869  7t7e49  9890  8t7e56  9896  9t7e63  9903  2exp7  13213  log2ublem2  16084  log2ublem3  16085  lgsdir2lem3  16149