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

Theorem pinn 8592
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 8586 . . 3  |-  N.  =  ( om  \  { (/) } )
2 difss 3379 . . 3  |-  ( om 
\  { (/) } ) 
C_  om
31, 2eqsstri 3284 . 2  |-  N.  C_  om
43sseli 3252 1  |-  ( A  e.  N.  ->  A  e.  om )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1710    \ cdif 3225   (/)c0 3531   {csn 3716   omcom 4738   N.cnpi 8556
This theorem is referenced by:  pion  8593  piord  8594  mulidpi  8600  addclpi  8606  mulclpi  8607  addcompi  8608  addasspi  8609  mulcompi  8610  mulasspi  8611  distrpi  8612  addcanpi  8613  mulcanpi  8614  addnidpi  8615  ltexpi  8616  ltapi  8617  ltmpi  8618  indpi  8621
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-v 2866  df-dif 3231  df-in 3235  df-ss 3242  df-ni 8586
  Copyright terms: Public domain W3C validator