Theorem pinn 10874

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   ∖ cdif 3903  ∅c0 4286  {csn 4591  ωcom 7864  Ncnpi 10840

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-dif 3909  df-ss 3923  df-ni 10868

This theorem is used by:  pion  10875  piord  10876  mulidpi  10882  addclpi  10888  mulclpi  10889  addcompi  10890  addasspi  10891  mulcompi  10892  mulasspi  10893  distrpi  10894  addcanpi  10895  mulcanpi  10896  addnidpi  10897  ltexpi  10898  ltapi  10899  ltmpi  10900  indpi  10903