Definition df-7 9377

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 9369	. 2 class 7
2		c6 9368	. . 3 class 6
3		c1 8186	. . 3 class 1
4		caddc 8188	. . 3 class +
5	2, 3, 4	co 6088	. 2 class ( 6 + 1 )
6	1, 5	wceq 1402	1 wff 7 = ( 6 + 1 )

This definition is used by:  7re  9396  7pos  9415  7m1e6  9437  6p1e7  9452  4p3e7  9458  5p2e7  9460  6p2e8  9463  7nn  9482  6lt7  9500  7p7e14  9871  8p7e15  9877  9p7e16  9884  9p8e17  9885  7t7e49  9906  8t7e56  9912  9t7e63  9919  2exp7  13243  7prm  13254  17prm  13260  37prm  13264  317prm  13269  log2ublem2  16222  log2ublem3  16223  bclbnd  16307  bposlem8  16318  lgsdir2lem3  16354