Theorem pinn 10789

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 10783	. . 3 ⊢ N = (ω ∖ {∅})
2		difss 4088	. . 3 ⊢ (ω ∖ {∅}) ⊆ ω
3	1, 2	eqsstri 3980	. 2 ⊢ N ⊆ ω
4	3	sseli 3929	1 ⊢ (𝐴 ∈ N → 𝐴 ∈ ω)

Syntax hints:   → wi 4   ∈ wcel 2113   ∖ cdif 3898  ∅c0 4285  {csn 4580  ωcom 7808  Ncnpi 10755

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-dif 3904  df-ss 3918  df-ni 10783

This theorem is referenced by:  pion  10790  piord  10791  mulidpi  10797  addclpi  10803  mulclpi  10804  addcompi  10805  addasspi  10806  mulcompi  10807  mulasspi  10808  distrpi  10809  addcanpi  10810  mulcanpi  10811  addnidpi  10812  ltexpi  10813  ltapi  10814  ltmpi  10815  indpi  10818