Definition df-7 9370

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 9362	. 2 class 7
2		c6 9361	. . 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  9389  7pos  9408  7m1e6  9430  6p1e7  9445  4p3e7  9451  5p2e7  9453  6p2e8  9456  7nn  9475  6lt7  9493  7p7e14  9864  8p7e15  9870  9p7e16  9877  9p8e17  9878  7t7e49  9899  8t7e56  9905  9t7e63  9912  2exp7  13234  7prm  13245  17prm  13251  37prm  13255  317prm  13260  log2ublem2  16141  log2ublem3  16142  bclbnd  16205  lgsdir2lem3  16247