Theorem pinn 10967

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 10961	. . 3 ⊢ N = (ω ∖ {∅})
2		difss 4072	. . 3 ⊢ (ω ∖ {∅}) ⊆ ω
3	1, 2	eqsstri 3954	. 2 ⊢ N ⊆ ω
4	3	sseli 3904	1 ⊢ (𝐴 ∈ N → 𝐴 ∈ ω)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144   ∖ cdif 4045  ∅c0 4278  {csn 4584  ωcom 7878  Ncnpi 10933

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-dif 4047  df-ni 10961

This theorem is used by:  pion  10968  piord  10969  mulidpi  10975  addclpi  10981  mulclpi  10982  addcompi  10983  addasspi  10984  mulcompi  10985  mulasspi  10986  distrpi  10987  addcanpi  10988  mulcanpi  10989  addnidpi  10990  ltexpi  10991  ltapi  10992  ltmpi  10993  indpi  10996