Definition df-7 12196

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 12188	. 2 class 7
2		c6 12187	. . 3 class 6
3		c1 11010	. . 3 class 1
4		caddc 11012	. . 3 class +
5	2, 3, 4	co 7349	. 2 class (6 + 1)
6	1, 5	wceq 1540	1 wff 7 = (6 + 1)

This definition is referenced by:  7nn  12220  7re  12221  7cn  12222  7pos  12239  7m1e6  12255  6p1e7  12271  4p3e7  12277  5p2e7  12279  6p2e8  12282  6lt7  12309  7p7e14  12670  8p7e15  12676  9p7e16  12683  9p8e17  12684  7t7e49  12705  8t7e56  12711  9t7e63  12718  2exp7  16999  7prm  17022  17prm  17028  37prm  17032  317prm  17037  log2ublem2  26855  log2ublem3  26856  bclbnd  27189  bposlem8  27200  lgsdir2lem3  27236  problem4  35651  3cubeslem3r  42670  rmydioph  42997  expdiophlem2  43005  fmtno5  47551  257prm  47555  127prm  47593  7odd  47706  stgoldbwt  47770