Theorem pinn 10831

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 10825	. . 3 ⊢ N = (ω ∖ {∅})
2		difss 4099	. . 3 ⊢ (ω ∖ {∅}) ⊆ ω
3	1, 2	eqsstri 3993	. 2 ⊢ N ⊆ ω
4	3	sseli 3942	1 ⊢ (𝐴 ∈ N → 𝐴 ∈ ω)

Syntax hints:   → wi 4   ∈ wcel 2109   ∖ cdif 3911  ∅c0 4296  {csn 4589  ωcom 7842  Ncnpi 10797

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-dif 3917  df-ss 3931  df-ni 10825

This theorem is referenced by:  pion  10832  piord  10833  mulidpi  10839  addclpi  10845  mulclpi  10846  addcompi  10847  addasspi  10848  mulcompi  10849  mulasspi  10850  distrpi  10851  addcanpi  10852  mulcanpi  10853  addnidpi  10854  ltexpi  10855  ltapi  10856  ltmpi  10857  indpi  10860