| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: One is a natural number. |
| Ref | Expression |
|---|---|
| 1onn |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-1o 5177 |
. 2
| |
| 2 | peano1 3971 |
. . 3
| |
| 3 | peano2 3972 |
. . 3
| |
| 4 | 2, 3 | ax-mp 7 |
. 2
|
| 5 | 1, 4 | eqeltri 1967 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: 2onn 5311 nneob 5312 snfi 5491 pwfi 5661 oancom 5740 card1 5983 unxpdomlem 5995 unxpdom2 5997 nnacda 6088 1pi 6163 1lt2pi 6184 indpi 6186 infxpidmlem1 8821 infxpidmlem12 8832 infpss 8843 infmap2 8850 setwoe 10170 bnj107 12452 top2usne 14898 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 1304 ax-gen 1305 ax-8 1306 ax-9 1307 ax-10 1308 ax-11 1309 ax-12 1310 ax-13 1311 ax-14 1312 ax-17 1317 ax-4 1319 ax-5o 1321 ax-6o 1324 ax-9o 1481 ax-10o 1500 ax-16 1580 ax-11o 1588 ax-ext 1865 ax-sep 3438 ax-nul 3445 ax-pow 3481 ax-pr 3524 ax-un 3790 |
| This theorem depends on definitions: df-bi 164 df-or 241 df-an 242 df-3or 859 df-3an 860 df-ex 1327 df-sb 1536 df-eu 1775 df-mo 1776 df-clab 1872 df-cleq 1877 df-clel 1880 df-ne 2019 df-ral 2109 df-rex 2110 df-rab 2112 df-v 2294 df-dif 2597 df-un 2600 df-in 2603 df-ss 2605 df-pss 2607 df-nul 2876 df-if 2983 df-pw 3035 df-sn 3049 df-pr 3050 df-tp 3052 df-op 3053 df-uni 3178 df-br 3339 df-opab 3396 df-tr 3412 df-eprel 3583 df-po 3591 df-so 3604 df-fr 3625 df-we 3644 df-ord 3660 df-on 3661 df-lim 3662 df-suc 3663 df-om 3950 df-1o 5177 |