ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  pinn Unicode version

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

Proof of Theorem pinn
StepHypRef Expression
1 df-ni 7076 . . 3  |-  N.  =  ( om  \  { (/) } )
2 difss 3170 . . 3  |-  ( om 
\  { (/) } ) 
C_  om
31, 2eqsstri 3097 . 2  |-  N.  C_  om
43sseli 3061 1  |-  ( A  e.  N.  ->  A  e.  om )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1463    \ cdif 3036   (/)c0 3331   {csn 3495   omcom 4472   N.cnpi 7044
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-v 2660  df-dif 3041  df-in 3045  df-ss 3052  df-ni 7076
This theorem is referenced by:  pion  7082  piord  7083  elni2  7086  mulidpi  7090  ltsopi  7092  pitric  7093  pitri3or  7094  ltdcpi  7095  addclpi  7099  mulclpi  7100  addcompig  7101  addasspig  7102  mulcompig  7103  mulasspig  7104  distrpig  7105  addcanpig  7106  mulcanpig  7107  addnidpig  7108  ltexpi  7109  ltapig  7110  ltmpig  7111  nnppipi  7115  enqdc  7133  archnqq  7189  prarloclemarch2  7191  enq0enq  7203  enq0sym  7204  enq0ref  7205  enq0tr  7206  nqnq0pi  7210  nqnq0  7213  addcmpblnq0  7215  mulcmpblnq0  7216  mulcanenq0ec  7217  addclnq0  7223  nqpnq0nq  7225  nqnq0a  7226  nqnq0m  7227  nq0m0r  7228  nq0a0  7229  nnanq0  7230  distrnq0  7231  mulcomnq0  7232  addassnq0lemcl  7233  addassnq0  7234  nq02m  7237  prarloclemlt  7265  prarloclemn  7271
  Copyright terms: Public domain W3C validator