![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-7 | Structured version Visualization version GIF version |
Description: Define the number 7. (Contributed by NM, 27-May-1999.) |
Ref | Expression |
---|---|
df-7 | ⊢ 7 = (6 + 1) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | c7 11550 | . 2 class 7 | |
2 | c6 11549 | . . 3 class 6 | |
3 | c1 10389 | . . 3 class 1 | |
4 | caddc 10391 | . . 3 class + | |
5 | 2, 3, 4 | co 7021 | . 2 class (6 + 1) |
6 | 1, 5 | wceq 1522 | 1 wff 7 = (6 + 1) |
Colors of variables: wff setvar class |
This definition is referenced by: 7nn 11582 7re 11583 7cn 11584 7pos 11601 7m1e6 11622 6p1e7 11638 4p3e7 11644 5p2e7 11646 6p2e8 11649 6lt7 11676 7p7e14 12032 8p7e15 12038 9p7e16 12045 9p8e17 12046 7t7e49 12067 8t7e56 12073 9t7e63 12080 7prm 16278 17prm 16284 37prm 16288 317prm 16293 log2ublem2 25212 log2ublem3 25213 bclbnd 25543 bposlem8 25554 lgsdir2lem3 25590 problem4 32526 rmydioph 39122 expdiophlem2 39130 fmtno5 43228 257prm 43232 2exp7 43271 127prm 43272 7odd 43386 stgoldbwt 43450 |
Copyright terms: Public domain | W3C validator |