Theorem pinn 10292

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 10286	. . 3 ⊢ N = (ω ∖ {∅})
2		difss 4106	. . 3 ⊢ (ω ∖ {∅}) ⊆ ω
3	1, 2	eqsstri 3999	. 2 ⊢ N ⊆ ω
4	3	sseli 3961	1 ⊢ (𝐴 ∈ N → 𝐴 ∈ ω)

Syntax hints:   → wi 4   ∈ wcel 2108   ∖ cdif 3931  ∅c0 4289  {csn 4559  ωcom 7572  Ncnpi 10258

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-v 3495  df-dif 3937  df-in 3941  df-ss 3950  df-ni 10286

This theorem is referenced by:  pion  10293  piord  10294  mulidpi  10300  addclpi  10306  mulclpi  10307  addcompi  10308  addasspi  10309  mulcompi  10310  mulasspi  10311  distrpi  10312  addcanpi  10313  mulcanpi  10314  addnidpi  10315  ltexpi  10316  ltapi  10317  ltmpi  10318  indpi  10321