Definition df-7 12244

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 12236	. 2 class 7
2		c6 12235	. . 3 class 6
3		c1 11035	. . 3 class 1
4		caddc 11037	. . 3 class +
5	2, 3, 4	co 7359	. 2 class (6 + 1)
6	1, 5	wceq 1548	1 wff 7 = (6 + 1)

This definition is referenced by:  7nn  12268  7re  12269  7cn  12270  7pos  12287  7m1e6  12303  6p1e7  12319  4p3e7  12325  5p2e7  12327  6p2e8  12330  6lt7  12357  7p7e14  12718  8p7e15  12724  9p7e16  12731  9p8e17  12732  7t7e49  12753  8t7e56  12759  9t7e63  12766  2exp7  17053  7prm  17076  17prm  17082  37prm  17086  317prm  17091  log2ublem2  26932  log2ublem3  26933  bclbnd  27264  bposlem8  27275  lgsdir2lem3  27311  problem4  35909  3cubeslem3r  43149  rmydioph  43472  expdiophlem2  43480  fmtno5  48047  257prm  48051  127prm  48089  7odd  48215  stgoldbwt  48279