Theorem pinn 10869

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 10863	. . 3 ⊢ N = (ω ∖ {∅})
2		difss 4089	. . 3 ⊢ (ω ∖ {∅}) ⊆ ω
3	1, 2	eqsstri 3982	. 2 ⊢ N ⊆ ω
4	3	sseli 3932	1 ⊢ (𝐴 ∈ N → 𝐴 ∈ ω)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2142   ∖ cdif 3901  ∅c0 4285  {csn 4588  ωcom 7860  Ncnpi 10835

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-dif 3907  df-ss 3921  df-ni 10863

This theorem is used by:  pion  10870  piord  10871  mulidpi  10877  addclpi  10883  mulclpi  10884  addcompi  10885  addasspi  10886  mulcompi  10887  mulasspi  10888  distrpi  10889  addcanpi  10890  mulcanpi  10891  addnidpi  10892  ltexpi  10893  ltapi  10894  ltmpi  10895  indpi  10898