| 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 12326 | . 2 class 7 | |
| 2 | c6 12325 | . . 3 class 6 | |
| 3 | c1 11156 | . . 3 class 1 | |
| 4 | caddc 11158 | . . 3 class + | |
| 5 | 2, 3, 4 | co 7431 | . 2 class (6 + 1) |
| 6 | 1, 5 | wceq 1540 | 1 wff 7 = (6 + 1) |
| Colors of variables: wff setvar class |
| This definition is referenced by: 7nn 12358 7re 12359 7cn 12360 7pos 12377 7m1e6 12398 6p1e7 12414 4p3e7 12420 5p2e7 12422 6p2e8 12425 6lt7 12452 7p7e14 12812 8p7e15 12818 9p7e16 12825 9p8e17 12826 7t7e49 12847 8t7e56 12853 9t7e63 12860 2exp7 17125 7prm 17148 17prm 17154 37prm 17158 317prm 17163 log2ublem2 26990 log2ublem3 26991 bclbnd 27324 bposlem8 27335 lgsdir2lem3 27371 problem4 35673 3cubeslem3r 42698 rmydioph 43026 expdiophlem2 43034 fmtno5 47544 257prm 47548 127prm 47586 7odd 47699 stgoldbwt 47763 |
| Copyright terms: Public domain | W3C validator |