Definition df-7 11365

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 11357	. 2 class 7
2		c6 11356	. . 3 class 6
3		c1 10218	. . 3 class 1
4		caddc 10220	. . 3 class +
5	2, 3, 4	co 6870	. 2 class (6 + 1)
6	1, 5	wceq 1637	1 wff 7 = (6 + 1)

This definition is referenced by:  7re  11383  7pos  11399  7m1e6  11420  6p1e7  11435  4p3e7  11441  5p2e7  11443  6p2e8  11446  7nn  11463  6lt7  11481  7p7e14  11834  8p7e15  11840  9p7e16  11847  9p8e17  11848  7t7e49  11869  8t7e56  11875  9t7e63  11882  7prm  16025  17prm  16031  37prm  16035  317prm  16040  log2ublem2  24884  log2ublem3  24885  bclbnd  25215  bposlem8  25226  lgsdir2lem3  25262  2lgslem3d  25334  problem4  31879  rmydioph  38076  expdiophlem2  38084  fmtno5  42038  257prm  42042  2exp7  42083  127prm  42084  7odd  42190  stgoldbwt  42233