Definition df-7 9102

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 9094	. 2 class 7
2		c6 9093	. . 3 class 6
3		c1 7928	. . 3 class 1
4		caddc 7930	. . 3 class +
5	2, 3, 4	co 5946	. 2 class ( 6 + 1 )
6	1, 5	wceq 1373	1 wff 7 = ( 6 + 1 )

This definition is referenced by:  7re  9121  7pos  9140  7m1e6  9162  6p1e7  9177  4p3e7  9183  5p2e7  9185  6p2e8  9188  7nn  9205  6lt7  9223  7p7e14  9584  8p7e15  9590  9p7e16  9597  9p8e17  9598  7t7e49  9619  8t7e56  9625  9t7e63  9632  2exp7  12790  lgsdir2lem3  15540