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  26890  log2ublem3  26891  bclbnd  27224  bposlem8  27235  lgsdir2lem3  27271  problem4  35648  3cubeslem3r  42668  rmydioph  42996  expdiophlem2  43004  fmtno5  47551  257prm  47555  127prm  47593  7odd  47706  stgoldbwt  47770