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

Theorem pinn 9052
Description: A positive integer is a natural number. (Contributed by NM, 15-Aug-1995.) (New usage is discouraged.)
Assertion
Ref Expression
pinn  |-  ( A  e.  N.  ->  A  e.  om )

Proof of Theorem pinn
StepHypRef Expression
1 df-ni 9046 . . 3  |-  N.  =  ( om  \  { (/) } )
2 difss 3488 . . 3  |-  ( om 
\  { (/) } ) 
C_  om
31, 2eqsstri 3391 . 2  |-  N.  C_  om
43sseli 3357 1  |-  ( A  e.  N.  ->  A  e.  om )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756    \ cdif 3330   (/)c0 3642   {csn 3882   omcom 6481   N.cnpi 9016
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-v 2979  df-dif 3336  df-in 3340  df-ss 3347  df-ni 9046
This theorem is referenced by:  pion  9053  piord  9054  mulidpi  9060  addclpi  9066  mulclpi  9067  addcompi  9068  addasspi  9069  mulcompi  9070  mulasspi  9071  distrpi  9072  addcanpi  9073  mulcanpi  9074  addnidpi  9075  ltexpi  9076  ltapi  9077  ltmpi  9078  indpi  9081
  Copyright terms: Public domain W3C validator