Theorem pinn 10792

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 10786	. . 3 ⊢ N = (ω ∖ {∅})
2		difss 4077	. . 3 ⊢ (ω ∖ {∅}) ⊆ ω
3	1, 2	eqsstri 3969	. 2 ⊢ N ⊆ ω
4	3	sseli 3918	1 ⊢ (𝐴 ∈ N → 𝐴 ∈ ω)

Syntax hints:   → wi 4   ∈ wcel 2114   ∖ cdif 3887  ∅c0 4274  {csn 4568  ωcom 7810  Ncnpi 10758

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-dif 3893  df-ss 3907  df-ni 10786

This theorem is referenced by:  pion  10793  piord  10794  mulidpi  10800  addclpi  10806  mulclpi  10807  addcompi  10808  addasspi  10809  mulcompi  10810  mulasspi  10811  distrpi  10812  addcanpi  10813  mulcanpi  10814  addnidpi  10815  ltexpi  10816  ltapi  10817  ltmpi  10818  indpi  10821