Definition df-7 12193

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 12185	. 2 class 7
2		c6 12184	. . 3 class 6
3		c1 11007	. . 3 class 1
4		caddc 11009	. . 3 class +
5	2, 3, 4	co 7346	. 2 class (6 + 1)
6	1, 5	wceq 1541	1 wff 7 = (6 + 1)

This definition is referenced by:  7nn  12217  7re  12218  7cn  12219  7pos  12236  7m1e6  12252  6p1e7  12268  4p3e7  12274  5p2e7  12276  6p2e8  12279  6lt7  12306  7p7e14  12667  8p7e15  12673  9p7e16  12680  9p8e17  12681  7t7e49  12702  8t7e56  12708  9t7e63  12715  2exp7  16999  7prm  17022  17prm  17028  37prm  17032  317prm  17037  log2ublem2  26884  log2ublem3  26885  bclbnd  27218  bposlem8  27229  lgsdir2lem3  27265  problem4  35712  3cubeslem3r  42790  rmydioph  43117  expdiophlem2  43125  fmtno5  47667  257prm  47671  127prm  47709  7odd  47822  stgoldbwt  47886