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

Theorem pinn 8711
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 8705 . . 3  |-  N.  =  ( om  \  { (/) } )
2 difss 3434 . . 3  |-  ( om 
\  { (/) } ) 
C_  om
31, 2eqsstri 3338 . 2  |-  N.  C_  om
43sseli 3304 1  |-  ( A  e.  N.  ->  A  e.  om )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1721    \ cdif 3277   (/)c0 3588   {csn 3774   omcom 4804   N.cnpi 8675
This theorem is referenced by:  pion  8712  piord  8713  mulidpi  8719  addclpi  8725  mulclpi  8726  addcompi  8727  addasspi  8728  mulcompi  8729  mulasspi  8730  distrpi  8731  addcanpi  8732  mulcanpi  8733  addnidpi  8734  ltexpi  8735  ltapi  8736  ltmpi  8737  indpi  8740
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-dif 3283  df-in 3287  df-ss 3294  df-ni 8705
  Copyright terms: Public domain W3C validator