Theorem pinn 10877

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 10871	. . 3 ⊢ N = (ω ∖ {∅})
2		difss 4132	. . 3 ⊢ (ω ∖ {∅}) ⊆ ω
3	1, 2	eqsstri 4017	. 2 ⊢ N ⊆ ω
4	3	sseli 3979	1 ⊢ (𝐴 ∈ N → 𝐴 ∈ ω)

Syntax hints:   → wi 4   ∈ wcel 2104   ∖ cdif 3946  ∅c0 4323  {csn 4629  ωcom 7859  Ncnpi 10843

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-dif 3952  df-in 3956  df-ss 3966  df-ni 10871

This theorem is referenced by:  pion  10878  piord  10879  mulidpi  10885  addclpi  10891  mulclpi  10892  addcompi  10893  addasspi  10894  mulcompi  10895  mulasspi  10896  distrpi  10897  addcanpi  10898  mulcanpi  10899  addnidpi  10900  ltexpi  10901  ltapi  10902  ltmpi  10903  indpi  10906