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

Theorem pinn 9245
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 9239 . . 3  |-  N.  =  ( om  \  { (/) } )
2 difss 3617 . . 3  |-  ( om 
\  { (/) } ) 
C_  om
31, 2eqsstri 3519 . 2  |-  N.  C_  om
43sseli 3485 1  |-  ( A  e.  N.  ->  A  e.  om )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1823    \ cdif 3458   (/)c0 3783   {csn 4016   omcom 6673   N.cnpi 9211
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3108  df-dif 3464  df-in 3468  df-ss 3475  df-ni 9239
This theorem is referenced by:  pion  9246  piord  9247  mulidpi  9253  addclpi  9259  mulclpi  9260  addcompi  9261  addasspi  9262  mulcompi  9263  mulasspi  9264  distrpi  9265  addcanpi  9266  mulcanpi  9267  addnidpi  9268  ltexpi  9269  ltapi  9270  ltmpi  9271  indpi  9274
  Copyright terms: Public domain W3C validator