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

Theorem pinn 10278
 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 10272 . . 3 N = (ω ∖ {∅})
2 difss 4087 . . 3 (ω ∖ {∅}) ⊆ ω
31, 2eqsstri 3980 . 2 N ⊆ ω
43sseli 3942 1 (𝐴N𝐴 ∈ ω)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∈ wcel 2114   ∖ cdif 3910  ∅c0 4269  {csn 4543  ωcom 7558  Ncnpi 10244 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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-12 2177  ax-ext 2792 This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2799  df-cleq 2813  df-clel 2891  df-v 3475  df-dif 3916  df-in 3920  df-ss 3930  df-ni 10272 This theorem is referenced by:  pion  10279  piord  10280  mulidpi  10286  addclpi  10292  mulclpi  10293  addcompi  10294  addasspi  10295  mulcompi  10296  mulasspi  10297  distrpi  10298  addcanpi  10299  mulcanpi  10300  addnidpi  10301  ltexpi  10302  ltapi  10303  ltmpi  10304  indpi  10307
 Copyright terms: Public domain W3C validator