Definition df-7 9371

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 9363	. 2 class 7
2		c6 9362	. . 3 class 6
3		c1 8181	. . 3 class 1
4		caddc 8183	. . 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  9390  7pos  9409  7m1e6  9431  6p1e7  9446  4p3e7  9452  5p2e7  9454  6p2e8  9457  7nn  9476  6lt7  9494  7p7e14  9865  8p7e15  9871  9p7e16  9878  9p8e17  9879  7t7e49  9900  8t7e56  9906  9t7e63  9913  2exp7  13237  7prm  13248  17prm  13254  37prm  13258  317prm  13263  log2ublem2  16183  log2ublem3  16184  bclbnd  16268  bposlem8  16279  lgsdir2lem3  16315