| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > df-5 | Structured version Visualization version GIF version | ||
| Description: Define the number 5. (Contributed by NM, 27-May-1999.) |
| Ref | Expression |
|---|---|
| df-5 | ⊢ 5 = (4 + 1) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | c5 12320 | . 2 class 5 | |
| 2 | c4 12319 | . . 3 class 4 | |
| 3 | c1 11152 | . . 3 class 1 | |
| 4 | caddc 11154 | . . 3 class + | |
| 5 | 2, 3, 4 | co 7429 | . 2 class (4 + 1) |
| 6 | 1, 5 | wceq 1540 | 1 wff 5 = (4 + 1) |
| Colors of variables: wff setvar class |
| This definition is referenced by: 5nn 12348 5re 12349 5cn 12350 5pos 12371 5m1e4 12392 4p1e5 12408 3p2e5 12413 4p2e6 12415 4lt5 12439 5p5e10 12800 6p5e11 12802 7p5e12 12806 8p5e13 12812 8p7e15 12814 9p5e14 12819 9p6e15 12820 5t5e25 12832 6t5e30 12836 7t5e35 12841 8t5e40 12847 9t5e45 12854 fldiv4p1lem1div2 13871 ef01bndlem 16216 prm23lt5 16848 5prm 17142 lt6abl 19909 log2ublem3 26981 ppiublem2 27237 bclbnd 27314 bposlem6 27323 bposlem9 27326 lgsdir2lem3 27361 2lgslem3c 27432 2lgsoddprmlem3c 27446 ex-exp 30459 ex-fac 30460 ex-bc 30461 3lexlogpow5ineq5 42054 aks4d1p1p7 42068 rmydioph 43019 expdiophlem2 43027 stoweidlem13 46019 fmtno5 47535 fmtnofac1 47548 31prm 47575 5odd 47688 sbgoldbo 47765 ackval50 48610 |
| Copyright terms: Public domain | W3C validator |