Definition df-7 9071

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 9063	. 2 class 7
2		c6 9062	. . 3 class 6
3		c1 7897	. . 3 class 1
4		caddc 7899	. . 3 class +
5	2, 3, 4	co 5925	. 2 class ( 6 + 1 )
6	1, 5	wceq 1364	1 wff 7 = ( 6 + 1 )

This definition is referenced by:  7re  9090  7pos  9109  7m1e6  9131  6p1e7  9146  4p3e7  9152  5p2e7  9154  6p2e8  9157  7nn  9174  6lt7  9192  7p7e14  9552  8p7e15  9558  9p7e16  9565  9p8e17  9566  7t7e49  9587  8t7e56  9593  9t7e63  9600  2exp7  12628  lgsdir2lem3  15355