Theorem pinn 10897

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 10891	. . 3 ⊢ N = (ω ∖ {∅})
2		difss 4116	. . 3 ⊢ (ω ∖ {∅}) ⊆ ω
3	1, 2	eqsstri 4010	. 2 ⊢ N ⊆ ω
4	3	sseli 3959	1 ⊢ (𝐴 ∈ N → 𝐴 ∈ ω)

Syntax hints:   → wi 4   ∈ wcel 2109   ∖ cdif 3928  ∅c0 4313  {csn 4606  ωcom 7866  Ncnpi 10863

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-dif 3934  df-ss 3948  df-ni 10891

This theorem is referenced by:  pion  10898  piord  10899  mulidpi  10905  addclpi  10911  mulclpi  10912  addcompi  10913  addasspi  10914  mulcompi  10915  mulasspi  10916  distrpi  10917  addcanpi  10918  mulcanpi  10919  addnidpi  10920  ltexpi  10921  ltapi  10922  ltmpi  10923  indpi  10926