Theorem pinn 10799

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 10793	. . 3 ⊢ N = (ω ∖ {∅})
2		difss 4073	. . 3 ⊢ (ω ∖ {∅}) ⊆ ω
3	1, 2	eqsstri 3968	. 2 ⊢ N ⊆ ω
4	3	sseli 3918	1 ⊢ (𝐴 ∈ N → 𝐴 ∈ ω)

Syntax hints:   → wi 4   ∈ wcel 2119   ∖ cdif 3887  ∅c0 4268  {csn 4562  ωcom 7813  Ncnpi 10765

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-dif 3893  df-ss 3907  df-ni 10793

This theorem is referenced by:  pion  10800  piord  10801  mulidpi  10807  addclpi  10813  mulclpi  10814  addcompi  10815  addasspi  10816  mulcompi  10817  mulasspi  10818  distrpi  10819  addcanpi  10820  mulcanpi  10821  addnidpi  10822  ltexpi  10823  ltapi  10824  ltmpi  10825  indpi  10828