Definition df-7 11706

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 11698	. 2 class 7
2		c6 11697	. . 3 class 6
3		c1 10538	. . 3 class 1
4		caddc 10540	. . 3 class +
5	2, 3, 4	co 7156	. 2 class (6 + 1)
6	1, 5	wceq 1537	1 wff 7 = (6 + 1)

This definition is referenced by:  7nn  11730  7re  11731  7cn  11732  7pos  11749  7m1e6  11770  6p1e7  11786  4p3e7  11792  5p2e7  11794  6p2e8  11797  6lt7  11824  7p7e14  12178  8p7e15  12184  9p7e16  12191  9p8e17  12192  7t7e49  12213  8t7e56  12219  9t7e63  12226  7prm  16444  17prm  16450  37prm  16454  317prm  16459  log2ublem2  25525  log2ublem3  25526  bclbnd  25856  bposlem8  25867  lgsdir2lem3  25903  problem4  32911  3cubeslem3r  39333  rmydioph  39660  expdiophlem2  39668  fmtno5  43768  257prm  43772  2exp7  43811  127prm  43812  7odd  43926  stgoldbwt  43990