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

Theorem pinn 10918
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 10912 . . 3 N = (ω ∖ {∅})
2 difss 4136 . . 3 (ω ∖ {∅}) ⊆ ω
31, 2eqsstri 4030 . 2 N ⊆ ω
43sseli 3979 1 (𝐴N𝐴 ∈ ω)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2108  cdif 3948  c0 4333  {csn 4626  ωcom 7887  Ncnpi 10884
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-dif 3954  df-ss 3968  df-ni 10912
This theorem is referenced by:  pion  10919  piord  10920  mulidpi  10926  addclpi  10932  mulclpi  10933  addcompi  10934  addasspi  10935  mulcompi  10936  mulasspi  10937  distrpi  10938  addcanpi  10939  mulcanpi  10940  addnidpi  10941  ltexpi  10942  ltapi  10943  ltmpi  10944  indpi  10947
  Copyright terms: Public domain W3C validator