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

Theorem pinn 9304
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 9298 . . 3  |-  N.  =  ( om  \  { (/) } )
2 difss 3592 . . 3  |-  ( om 
\  { (/) } ) 
C_  om
31, 2eqsstri 3494 . 2  |-  N.  C_  om
43sseli 3460 1  |-  ( A  e.  N.  ->  A  e.  om )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1868    \ cdif 3433   (/)c0 3761   {csn 3996   omcom 6703   N.cnpi 9270
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-v 3083  df-dif 3439  df-in 3443  df-ss 3450  df-ni 9298
This theorem is referenced by:  pion  9305  piord  9306  mulidpi  9312  addclpi  9318  mulclpi  9319  addcompi  9320  addasspi  9321  mulcompi  9322  mulasspi  9323  distrpi  9324  addcanpi  9325  mulcanpi  9326  addnidpi  9327  ltexpi  9328  ltapi  9329  ltmpi  9330  indpi  9333
  Copyright terms: Public domain W3C validator