| 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 4191 |
. 2
| |
| 2 | peano1 3206 |
. . 3
| |
| 3 | peano2 3207 |
. . 3
| |
| 4 | 2, 3 | ax-mp 7 |
. 2
|
| 5 | 1, 4 | eqeltri 1591 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: 2onn 4312 nneob 4313 snfi 4493 pwfi 4631 oancom 4695 card1 4896 unxpdomlem 4908 unxpdom2 4910 1pi 5076 1lt2pi 5097 indpi 5099 infxpidmlem1 7644 infxpidmlem12 7655 infpss 7666 infmap2 7673 setwoe 10640 top2usne 10643 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 1003 ax-gen 1004 ax-8 1005 ax-10 1007 ax-11 1008 ax-12 1009 ax-13 1010 ax-14 1011 ax-17 1012 ax-4 1014 ax-5o 1016 ax-6o 1019 ax-9o 1164 ax-10o 1182 ax-16 1252 ax-11o 1260 ax-ext 1504 ax-sep 2758 ax-nul 2765 ax-pow 2798 ax-pr 2835 ax-un 2922 |
| This theorem depends on definitions: df-bi 154 df-or 231 df-an 232 df-3or 788 df-3an 789 df-ex 1022 df-sb 1214 df-eu 1424 df-mo 1425 df-clab 1510 df-cleq 1515 df-clel 1518 df-ne 1634 df-ral 1696 df-rex 1697 df-v 1859 df-dif 2100 df-un 2101 df-in 2102 df-ss 2104 df-nul 2332 df-if 2414 df-pw 2454 df-sn 2464 df-pr 2465 df-tp 2467 df-op 2468 df-uni 2558 df-br 2675 df-opab 2722 df-tr 2736 df-eprel 2888 df-po 2896 df-so 2906 df-fr 2974 df-we 2991 df-ord 3008 df-on 3009 df-lim 3010 df-suc 3011 df-om 3189 df-1o 4191 |