Theorem pinn 10838

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 10832	. . 3 ⊢ N = (ω ∖ {∅})
2		difss 4102	. . 3 ⊢ (ω ∖ {∅}) ⊆ ω
3	1, 2	eqsstri 3996	. 2 ⊢ N ⊆ ω
4	3	sseli 3945	1 ⊢ (𝐴 ∈ N → 𝐴 ∈ ω)

Syntax hints:   → wi 4   ∈ wcel 2109   ∖ cdif 3914  ∅c0 4299  {csn 4592  ωcom 7845  Ncnpi 10804

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-dif 3920  df-ss 3934  df-ni 10832

This theorem is referenced by:  pion  10839  piord  10840  mulidpi  10846  addclpi  10852  mulclpi  10853  addcompi  10854  addasspi  10855  mulcompi  10856  mulasspi  10857  distrpi  10858  addcanpi  10859  mulcanpi  10860  addnidpi  10861  ltexpi  10862  ltapi  10863  ltmpi  10864  indpi  10867