Theorem pinn 10791

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 10785	. . 3 ⊢ N = (ω ∖ {∅})
2		difss 4089	. . 3 ⊢ (ω ∖ {∅}) ⊆ ω
3	1, 2	eqsstri 3984	. 2 ⊢ N ⊆ ω
4	3	sseli 3933	1 ⊢ (𝐴 ∈ N → 𝐴 ∈ ω)

Syntax hints:   → wi 4   ∈ wcel 2109   ∖ cdif 3902  ∅c0 4286  {csn 4579  ωcom 7806  Ncnpi 10757

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 3440  df-dif 3908  df-ss 3922  df-ni 10785

This theorem is referenced by:  pion  10792  piord  10793  mulidpi  10799  addclpi  10805  mulclpi  10806  addcompi  10807  addasspi  10808  mulcompi  10809  mulasspi  10810  distrpi  10811  addcanpi  10812  mulcanpi  10813  addnidpi  10814  ltexpi  10815  ltapi  10816  ltmpi  10817  indpi  10820