Theorem pinn 10289

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 10283	. . 3 ⊢ N = (ω ∖ {∅})
2		difss 4059	. . 3 ⊢ (ω ∖ {∅}) ⊆ ω
3	1, 2	eqsstri 3949	. 2 ⊢ N ⊆ ω
4	3	sseli 3911	1 ⊢ (𝐴 ∈ N → 𝐴 ∈ ω)

Syntax hints:   → wi 4   ∈ wcel 2111   ∖ cdif 3878  ∅c0 4243  {csn 4525  ωcom 7560  Ncnpi 10255

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-dif 3884  df-in 3888  df-ss 3898  df-ni 10283

This theorem is referenced by:  pion  10290  piord  10291  mulidpi  10297  addclpi  10303  mulclpi  10304  addcompi  10305  addasspi  10306  mulcompi  10307  mulasspi  10308  distrpi  10309  addcanpi  10310  mulcanpi  10311  addnidpi  10312  ltexpi  10313  ltapi  10314  ltmpi  10315  indpi  10318