Theorem pinn 10829

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 10823	. . 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 7840  Ncnpi 10795

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 10823

This theorem is referenced by:  pion  10830  piord  10831  mulidpi  10837  addclpi  10843  mulclpi  10844  addcompi  10845  addasspi  10846  mulcompi  10847  mulasspi  10848  distrpi  10849  addcanpi  10850  mulcanpi  10851  addnidpi  10852  ltexpi  10853  ltapi  10854  ltmpi  10855  indpi  10858