| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > pinn | Structured version Visualization version GIF version | ||
| Description: A positive integer is a natural number. (Contributed by NM, 15-Aug-1995.) (New usage is discouraged.) |
| Ref | Expression |
|---|---|
| pinn | ⊢ (𝐴 ∈ N → 𝐴 ∈ ω) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-ni 10824 | . . 3 ⊢ N = (ω ∖ {∅}) | |
| 2 | difss 4087 | . . 3 ⊢ (ω ∖ {∅}) ⊆ ω | |
| 3 | 1, 2 | eqsstri 3980 | . 2 ⊢ N ⊆ ω |
| 4 | 3 | sseli 3930 | 1 ⊢ (𝐴 ∈ N → 𝐴 ∈ ω) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∈ wcel 2141 ∖ cdif 3899 ∅c0 4283 {csn 4579 ωcom 7841 Ncnpi 10796 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-ext 2733 |
| This theorem depends on definitions: df-bi 209 df-an 400 df-tru 1562 df-ex 1799 df-sb 2090 df-clab 2740 df-cleq 2753 df-clel 2836 df-v 3455 df-dif 3905 df-ss 3919 df-ni 10824 |
| This theorem is referenced by: pion 10831 piord 10832 mulidpi 10838 addclpi 10844 mulclpi 10845 addcompi 10846 addasspi 10847 mulcompi 10848 mulasspi 10849 distrpi 10850 addcanpi 10851 mulcanpi 10852 addnidpi 10853 ltexpi 10854 ltapi 10855 ltmpi 10856 indpi 10859 |
| Copyright terms: Public domain | W3C validator |