Definition df-7 12361

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 12353	. 2 class 7
2		c6 12352	. . 3 class 6
3		c1 11185	. . 3 class 1
4		caddc 11187	. . 3 class +
5	2, 3, 4	co 7448	. 2 class (6 + 1)
6	1, 5	wceq 1537	1 wff 7 = (6 + 1)

This definition is referenced by:  7nn  12385  7re  12386  7cn  12387  7pos  12404  7m1e6  12425  6p1e7  12441  4p3e7  12447  5p2e7  12449  6p2e8  12452  6lt7  12479  7p7e14  12837  8p7e15  12843  9p7e16  12850  9p8e17  12851  7t7e49  12872  8t7e56  12878  9t7e63  12885  2exp7  17135  7prm  17158  17prm  17164  37prm  17168  317prm  17173  log2ublem2  27008  log2ublem3  27009  bclbnd  27342  bposlem8  27353  lgsdir2lem3  27389  problem4  35636  3cubeslem3r  42643  rmydioph  42971  expdiophlem2  42979  fmtno5  47431  257prm  47435  127prm  47473  7odd  47586  stgoldbwt  47650