Definition df-7 12211

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 12203	. 2 class 7
2		c6 12202	. . 3 class 6
3		c1 11025	. . 3 class 1
4		caddc 11027	. . 3 class +
5	2, 3, 4	co 7356	. 2 class (6 + 1)
6	1, 5	wceq 1541	1 wff 7 = (6 + 1)

This definition is referenced by:  7nn  12235  7re  12236  7cn  12237  7pos  12254  7m1e6  12270  6p1e7  12286  4p3e7  12292  5p2e7  12294  6p2e8  12297  6lt7  12324  7p7e14  12684  8p7e15  12690  9p7e16  12697  9p8e17  12698  7t7e49  12719  8t7e56  12725  9t7e63  12732  2exp7  17013  7prm  17036  17prm  17042  37prm  17046  317prm  17051  log2ublem2  26911  log2ublem3  26912  bclbnd  27245  bposlem8  27256  lgsdir2lem3  27292  problem4  35811  3cubeslem3r  42871  rmydioph  43198  expdiophlem2  43206  fmtno5  47745  257prm  47749  127prm  47787  7odd  47900  stgoldbwt  47964