![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > pinn | GIF version |
Description: A positive integer is a natural number. (Contributed by NM, 15-Aug-1995.) |
Ref | Expression |
---|---|
pinn | ⊢ (𝐴 ∈ N → 𝐴 ∈ ω) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ni 7306 | . . 3 ⊢ N = (ω ∖ {∅}) | |
2 | difss 3263 | . . 3 ⊢ (ω ∖ {∅}) ⊆ ω | |
3 | 1, 2 | eqsstri 3189 | . 2 ⊢ N ⊆ ω |
4 | 3 | sseli 3153 | 1 ⊢ (𝐴 ∈ N → 𝐴 ∈ ω) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 2148 ∖ cdif 3128 ∅c0 3424 {csn 3594 ωcom 4591 Ncnpi 7274 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 614 ax-in2 615 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-tru 1356 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-v 2741 df-dif 3133 df-in 3137 df-ss 3144 df-ni 7306 |
This theorem is referenced by: pion 7312 piord 7313 elni2 7316 mulidpi 7320 ltsopi 7322 pitric 7323 pitri3or 7324 ltdcpi 7325 addclpi 7329 mulclpi 7330 addcompig 7331 addasspig 7332 mulcompig 7333 mulasspig 7334 distrpig 7335 addcanpig 7336 mulcanpig 7337 addnidpig 7338 ltexpi 7339 ltapig 7340 ltmpig 7341 nnppipi 7345 enqdc 7363 archnqq 7419 prarloclemarch2 7421 enq0enq 7433 enq0sym 7434 enq0ref 7435 enq0tr 7436 nqnq0pi 7440 nqnq0 7443 addcmpblnq0 7445 mulcmpblnq0 7446 mulcanenq0ec 7447 addclnq0 7453 nqpnq0nq 7455 nqnq0a 7456 nqnq0m 7457 nq0m0r 7458 nq0a0 7459 nnanq0 7460 distrnq0 7461 mulcomnq0 7462 addassnq0lemcl 7463 addassnq0 7464 nq02m 7467 prarloclemlt 7495 prarloclemn 7501 |
Copyright terms: Public domain | W3C validator |