Definition df-7 12230

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 12222	. 2 class 7
2		c6 12221	. . 3 class 6
3		c1 11045	. . 3 class 1
4		caddc 11047	. . 3 class +
5	2, 3, 4	co 7369	. 2 class (6 + 1)
6	1, 5	wceq 1540	1 wff 7 = (6 + 1)

This definition is referenced by:  7nn  12254  7re  12255  7cn  12256  7pos  12273  7m1e6  12289  6p1e7  12305  4p3e7  12311  5p2e7  12313  6p2e8  12316  6lt7  12343  7p7e14  12704  8p7e15  12710  9p7e16  12717  9p8e17  12718  7t7e49  12739  8t7e56  12745  9t7e63  12752  2exp7  17034  7prm  17057  17prm  17063  37prm  17067  317prm  17072  log2ublem2  26833  log2ublem3  26834  bclbnd  27167  bposlem8  27178  lgsdir2lem3  27214  problem4  35628  3cubeslem3r  42648  rmydioph  42976  expdiophlem2  42984  fmtno5  47531  257prm  47535  127prm  47573  7odd  47686  stgoldbwt  47750