Theorem pinn 10302

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 10296	. . 3 ⊢ N = (ω ∖ {∅})
2		difss 4110	. . 3 ⊢ (ω ∖ {∅}) ⊆ ω
3	1, 2	eqsstri 4003	. 2 ⊢ N ⊆ ω
4	3	sseli 3965	1 ⊢ (𝐴 ∈ N → 𝐴 ∈ ω)

Syntax hints:   → wi 4   ∈ wcel 2114   ∖ cdif 3935  ∅c0 4293  {csn 4569  ωcom 7582  Ncnpi 10268

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-dif 3941  df-in 3945  df-ss 3954  df-ni 10296

This theorem is referenced by:  pion  10303  piord  10304  mulidpi  10310  addclpi  10316  mulclpi  10317  addcompi  10318  addasspi  10319  mulcompi  10320  mulasspi  10321  distrpi  10322  addcanpi  10323  mulcanpi  10324  addnidpi  10325  ltexpi  10326  ltapi  10327  ltmpi  10328  indpi  10331