Theorem pinn 10869

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 10863	. . 3 ⊢ N = (ω ∖ {∅})
2		difss 4123	. . 3 ⊢ (ω ∖ {∅}) ⊆ ω
3	1, 2	eqsstri 4008	. 2 ⊢ N ⊆ ω
4	3	sseli 3970	1 ⊢ (𝐴 ∈ N → 𝐴 ∈ ω)

Syntax hints:   → wi 4   ∈ wcel 2098   ∖ cdif 3937  ∅c0 4314  {csn 4620  ωcom 7848  Ncnpi 10835

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-v 3468  df-dif 3943  df-in 3947  df-ss 3957  df-ni 10863

This theorem is referenced by:  pion  10870  piord  10871  mulidpi  10877  addclpi  10883  mulclpi  10884  addcompi  10885  addasspi  10886  mulcompi  10887  mulasspi  10888  distrpi  10889  addcanpi  10890  mulcanpi  10891  addnidpi  10892  ltexpi  10893  ltapi  10894  ltmpi  10895  indpi  10898