Theorem pinn 10830

Description: A positive integer is a natural number. (Contributed by NM, 15-Aug-1995.) (New usage is discouraged.)

Assertion

Ref	Expression
pinn	⊢ (𝐴 ∈ N → 𝐴 ∈ ω)

Proof of Theorem pinn

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 → 𝐴 ∈ ω)

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