Theorem pinn 10379

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 10373	. . 3 ⊢ N = (ω ∖ {∅})
2		difss 4023	. . 3 ⊢ (ω ∖ {∅}) ⊆ ω
3	1, 2	eqsstri 3912	. 2 ⊢ N ⊆ ω
4	3	sseli 3874	1 ⊢ (𝐴 ∈ N → 𝐴 ∈ ω)

Syntax hints:   → wi 4   ∈ wcel 2113   ∖ cdif 3841  ∅c0 4212  {csn 4517  ωcom 7600  Ncnpi 10345

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-ex 1787  df-sb 2074  df-clab 2717  df-cleq 2730  df-clel 2811  df-v 3400  df-dif 3847  df-in 3851  df-ss 3861  df-ni 10373

This theorem is referenced by:  pion  10380  piord  10381  mulidpi  10387  addclpi  10393  mulclpi  10394  addcompi  10395  addasspi  10396  mulcompi  10397  mulasspi  10398  distrpi  10399  addcanpi  10400  mulcanpi  10401  addnidpi  10402  ltexpi  10403  ltapi  10404  ltmpi  10405  indpi  10408