Definition df-7 9185

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 9177	. 2 class 7
2		c6 9176	. . 3 class 6
3		c1 8011	. . 3 class 1
4		caddc 8013	. . 3 class +
5	2, 3, 4	co 6007	. 2 class (6 + 1)
6	1, 5	wceq 1395	1 wff 7 = (6 + 1)

This definition is referenced by:  7re  9204  7pos  9223  7m1e6  9245  6p1e7  9260  4p3e7  9266  5p2e7  9268  6p2e8  9271  7nn  9288  6lt7  9306  7p7e14  9667  8p7e15  9673  9p7e16  9680  9p8e17  9681  7t7e49  9702  8t7e56  9708  9t7e63  9715  2exp7  12972  lgsdir2lem3  15724