Definition df-7 12287

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 12279	. 2 class 7
2		c6 12278	. . 3 class 6
3		c1 11076	. . 3 class 1
4		caddc 11078	. . 3 class +
5	2, 3, 4	co 7398	. 2 class (6 + 1)
6	1, 5	wceq 1562	1 wff 7 = (6 + 1)

This definition is referenced by:  7nn  12312  7re  12313  7cn  12314  7m1e6  12351  6p1e7  12367  4p3e7  12373  5p2e7  12375  6p2e8  12378  6lt7  12408  7p7e14  12774  8p7e15  12780  9p7e16  12787  9p8e17  12788  7t7e49  12809  8t7e56  12815  9t7e63  12822  2exp7  17125  7prm  17148  17prm  17155  37prm  17159  317prm  17164  log2ublem2  27014  log2ublem3  27015  bclbnd  27346  bposlem8  27357  lgsdir2lem3  27393  problem4  36023  3cubeslem3r  43273  rmydioph  43596  expdiophlem2  43604  fmtno5  48171  257prm  48175  127prm  48213  7odd  48339  stgoldbwt  48403