Theorem pinn 10565

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 10559	. . 3 ⊢ N = (ω ∖ {∅})
2		difss 4062	. . 3 ⊢ (ω ∖ {∅}) ⊆ ω
3	1, 2	eqsstri 3951	. 2 ⊢ N ⊆ ω
4	3	sseli 3913	1 ⊢ (𝐴 ∈ N → 𝐴 ∈ ω)

Syntax hints:   → wi 4   ∈ wcel 2108   ∖ cdif 3880  ∅c0 4253  {csn 4558  ωcom 7687  Ncnpi 10531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-dif 3886  df-in 3890  df-ss 3900  df-ni 10559

This theorem is referenced by:  pion  10566  piord  10567  mulidpi  10573  addclpi  10579  mulclpi  10580  addcompi  10581  addasspi  10582  mulcompi  10583  mulasspi  10584  distrpi  10585  addcanpi  10586  mulcanpi  10587  addnidpi  10588  ltexpi  10589  ltapi  10590  ltmpi  10591  indpi  10594