| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > df-8 | Structured version Visualization version GIF version | ||
| Description: Define the number 8. (Contributed by NM, 27-May-1999.) |
| Ref | Expression |
|---|---|
| df-8 | ⊢ 8 = (7 + 1) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | c8 12327 | . 2 class 8 | |
| 2 | c7 12326 | . . 3 class 7 | |
| 3 | c1 11156 | . . 3 class 1 | |
| 4 | caddc 11158 | . . 3 class + | |
| 5 | 2, 3, 4 | co 7431 | . 2 class (7 + 1) |
| 6 | 1, 5 | wceq 1540 | 1 wff 8 = (7 + 1) |
| Colors of variables: wff setvar class |
| This definition is referenced by: 8nn 12361 8re 12362 8cn 12363 8pos 12378 8m1e7 12399 7p1e8 12415 4p4e8 12421 5p3e8 12423 6p2e8 12425 7p2e9 12427 7lt8 12458 8p8e16 12819 9p8e17 12826 9p9e18 12827 8t8e64 12854 9t8e72 12861 log2ub 26992 3cubeslem3r 42698 rmydioph 43026 |
| Copyright terms: Public domain | W3C validator |