![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 1onn | GIF version |
Description: One is a natural number. (Contributed by NM, 29-Oct-1995.) |
Ref | Expression |
---|---|
1onn | ⊢ 1o ∈ ω |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-1o 6353 | . 2 ⊢ 1o = suc ∅ | |
2 | peano1 4547 | . . 3 ⊢ ∅ ∈ ω | |
3 | peano2 4548 | . . 3 ⊢ (∅ ∈ ω → suc ∅ ∈ ω) | |
4 | 2, 3 | ax-mp 5 | . 2 ⊢ suc ∅ ∈ ω |
5 | 1, 4 | eqeltri 2227 | 1 ⊢ 1o ∈ ω |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 2125 ∅c0 3390 suc csuc 4320 ωcom 4543 1oc1o 6346 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 604 ax-in2 605 ax-io 699 ax-5 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1481 ax-10 1482 ax-11 1483 ax-i12 1484 ax-bndl 1486 ax-4 1487 ax-17 1503 ax-i9 1507 ax-ial 1511 ax-i5r 1512 ax-13 2127 ax-14 2128 ax-ext 2136 ax-sep 4078 ax-nul 4086 ax-pow 4130 ax-pr 4164 ax-un 4388 |
This theorem depends on definitions: df-bi 116 df-3an 965 df-tru 1335 df-nf 1438 df-sb 1740 df-clab 2141 df-cleq 2147 df-clel 2150 df-nfc 2285 df-ral 2437 df-rex 2438 df-v 2711 df-dif 3100 df-un 3102 df-in 3104 df-ss 3111 df-nul 3391 df-pw 3541 df-sn 3562 df-pr 3563 df-uni 3769 df-int 3804 df-suc 4326 df-iom 4544 df-1o 6353 |
This theorem is referenced by: 2onn 6457 nnm2 6461 nnaordex 6463 snfig 6748 snnen2og 6793 1nen2 6795 unfiexmid 6851 en1eqsn 6881 omp1eomlem 7024 fodjum 7068 fodju0 7069 en2eleq 7109 en2other2 7110 exmidfodomrlemr 7116 exmidfodomrlemrALT 7117 1pi 7214 1lt2pi 7239 archnqq 7316 nq0m0r 7355 nq02m 7364 prarloclemlt 7392 prarloclemlo 7393 1tonninf 10317 hash2 10663 012of 13506 pwle2 13509 peano3nninf 13519 nninfall 13522 nninfsellemdc 13523 nninfsellemeq 13527 nninfsellemeqinf 13529 nninffeq 13533 sbthom 13538 isomninnlem 13542 iswomninnlem 13561 ismkvnnlem 13564 |
Copyright terms: Public domain | W3C validator |