Theorem pinn 10887

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 10881	. . 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 7862  Ncnpi 10853

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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-dif 3902  df-ss 3916  df-ni 10881

This theorem is used by:  pion  10888  piord  10889  mulidpi  10895  addclpi  10901  mulclpi  10902  addcompi  10903  addasspi  10904  mulcompi  10905  mulasspi  10906  distrpi  10907  addcanpi  10908  mulcanpi  10909  addnidpi  10910  ltexpi  10911  ltapi  10912  ltmpi  10913  indpi  10916