Theorem pinn 10864

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 10858	. . 3 ⊢ N = (ω ∖ {∅})
2		difss 4091	. . 3 ⊢ (ω ∖ {∅}) ⊆ ω
3	1, 2	eqsstri 3984	. 2 ⊢ N ⊆ ω
4	3	sseli 3934	1 ⊢ (𝐴 ∈ N → 𝐴 ∈ ω)

Syntax hints:   → wi 4   ∈ wcel 2143   ∖ cdif 3903  ∅c0 4287  {csn 4590  ωcom 7863  Ncnpi 10830

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-dif 3909  df-ss 3923  df-ni 10858

This theorem is referenced by:  pion  10865  piord  10866  mulidpi  10872  addclpi  10878  mulclpi  10879  addcompi  10880  addasspi  10881  mulcompi  10882  mulasspi  10883  distrpi  10884  addcanpi  10885  mulcanpi  10886  addnidpi  10887  ltexpi  10888  ltapi  10889  ltmpi  10890  indpi  10893