Theorem pinn 10956

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 10950	. . 3 ⊢ N = (ω ∖ {∅})
2		difss 4083	. . 3 ⊢ (ω ∖ {∅}) ⊆ ω
3	1, 2	eqsstri 3977	. 2 ⊢ N ⊆ ω
4	3	sseli 3927	1 ⊢ (𝐴 ∈ N → 𝐴 ∈ ω)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ∖ cdif 3896  ∅c0 4279  {csn 4584  ωcom 7875  Ncnpi 10922

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-dif 3902  df-ss 3916  df-ni 10950

This theorem is used by:  pion  10957  piord  10958  mulidpi  10964  addclpi  10970  mulclpi  10971  addcompi  10972  addasspi  10973  mulcompi  10974  mulasspi  10975  distrpi  10976  addcanpi  10977  mulcanpi  10978  addnidpi  10979  ltexpi  10980  ltapi  10981  ltmpi  10982  indpi  10985