Definition df-7 11122

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 11113	. 2 class 7
2		c6 11112	. . 3 class 6
3		c1 9975	. . 3 class 1
4		caddc 9977	. . 3 class +
5	2, 3, 4	co 6690	. 2 class (6 + 1)
6	1, 5	wceq 1523	1 wff 7 = (6 + 1)

This definition is referenced by:  7re  11141  7pos  11158  7m1e6  11179  6p1e7  11194  4p3e7  11201  5p2e7  11203  6p2e8  11207  7nn  11228  6lt7  11247  7p7e14  11647  8p7e15  11655  9p7e16  11663  9p8e17  11664  7t7e49  11691  8t7e56  11699  9t7e63  11706  7prm  15864  17prm  15871  37prm  15875  317prm  15880  log2ublem2  24719  log2ublem3  24720  bclbnd  25050  bposlem8  25061  lgsdir2lem3  25097  2lgslem3d  25169  problem4  31688  rmydioph  37898  expdiophlem2  37906  fmtno5  41794  257prm  41798  2exp7  41839  127prm  41840  7odd  41946  stgoldbwt  41989