Theorem pinn 10947

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 10941	. . 3 ⊢ N = (ω ∖ {∅})
2		difss 4159	. . 3 ⊢ (ω ∖ {∅}) ⊆ ω
3	1, 2	eqsstri 4043	. 2 ⊢ N ⊆ ω
4	3	sseli 4004	1 ⊢ (𝐴 ∈ N → 𝐴 ∈ ω)

Syntax hints:   → wi 4   ∈ wcel 2108   ∖ cdif 3973  ∅c0 4352  {csn 4648  ωcom 7903  Ncnpi 10913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-dif 3979  df-ss 3993  df-ni 10941

This theorem is referenced by:  pion  10948  piord  10949  mulidpi  10955  addclpi  10961  mulclpi  10962  addcompi  10963  addasspi  10964  mulcompi  10965  mulasspi  10966  distrpi  10967  addcanpi  10968  mulcanpi  10969  addnidpi  10970  ltexpi  10971  ltapi  10972  ltmpi  10973  indpi  10976