MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pinn Structured version   Visualization version   GIF version

Theorem pinn 10829
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
StepHypRef Expression
1 df-ni 10823 . . 3 N = (ω ∖ {∅})
2 difss 4087 . . 3 (ω ∖ {∅}) ⊆ ω
31, 2eqsstri 3980 . 2 N ⊆ ω
43sseli 3930 1 (𝐴N𝐴 ∈ ω)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2141  cdif 3899  c0 4283  {csn 4579  ωcom 7840  Ncnpi 10795
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733
This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-dif 3905  df-ss 3919  df-ni 10823
This theorem is referenced by:  pion  10830  piord  10831  mulidpi  10837  addclpi  10843  mulclpi  10844  addcompi  10845  addasspi  10846  mulcompi  10847  mulasspi  10848  distrpi  10849  addcanpi  10850  mulcanpi  10851  addnidpi  10852  ltexpi  10853  ltapi  10854  ltmpi  10855  indpi  10858
  Copyright terms: Public domain W3C validator