Theorem pinn 10859

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 10853	. . 3 ⊢ N = (ω ∖ {∅})
2		difss 4098	. . 3 ⊢ (ω ∖ {∅}) ⊆ ω
3	1, 2	eqsstri 3991	. 2 ⊢ N ⊆ ω
4	3	sseli 3941	1 ⊢ (𝐴 ∈ N → 𝐴 ∈ ω)

Syntax hints:   → wi 4   ∈ wcel 2149   ∖ cdif 3910  ∅c0 4294  {csn 4591  ωcom 7858  Ncnpi 10825

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-dif 3916  df-ss 3930  df-ni 10853

This theorem is referenced by:  pion  10860  piord  10861  mulidpi  10867  addclpi  10873  mulclpi  10874  addcompi  10875  addasspi  10876  mulcompi  10877  mulasspi  10878  distrpi  10879  addcanpi  10880  mulcanpi  10881  addnidpi  10882  ltexpi  10883  ltapi  10884  ltmpi  10885  indpi  10888