Definition df-7 12324

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 12316	. 2 class 7
2		c6 12315	. . 3 class 6
3		c1 11148	. . 3 class 1
4		caddc 11150	. . 3 class +
5	2, 3, 4	co 7414	. 2 class (6 + 1)
6	1, 5	wceq 1534	1 wff 7 = (6 + 1)

This definition is referenced by:  7nn  12348  7re  12349  7cn  12350  7pos  12367  7m1e6  12388  6p1e7  12404  4p3e7  12410  5p2e7  12412  6p2e8  12415  6lt7  12442  7p7e14  12800  8p7e15  12806  9p7e16  12813  9p8e17  12814  7t7e49  12835  8t7e56  12841  9t7e63  12848  2exp7  17083  7prm  17106  17prm  17112  37prm  17116  317prm  17121  log2ublem2  26970  log2ublem3  26971  bclbnd  27304  bposlem8  27315  lgsdir2lem3  27351  problem4  35507  3cubeslem3r  42379  rmydioph  42707  expdiophlem2  42715  fmtno5  47163  257prm  47167  127prm  47205  7odd  47318  stgoldbwt  47382