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

Theorem pinn 6435
Description: A positive integer is a natural number. (Contributed by NM, 15-Aug-1995.)
Assertion
Ref Expression
pinn (𝐴N𝐴 ∈ ω)

Proof of Theorem pinn
StepHypRef Expression
1 df-ni 6430 . . 3 N = (ω ∖ {∅})
2 difss 3095 . . 3 (ω ∖ {∅}) ⊆ ω
31, 2eqsstri 3000 . 2 N ⊆ ω
43sseli 2966 1 (𝐴N𝐴 ∈ ω)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1407  cdif 2939  c0 3249  {csn 3400  ωcom 4338  Ncnpi 6398
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-in1 552  ax-in2 553  ax-io 638  ax-5 1350  ax-7 1351  ax-gen 1352  ax-ie1 1396  ax-ie2 1397  ax-8 1409  ax-10 1410  ax-11 1411  ax-i12 1412  ax-bndl 1413  ax-4 1414  ax-17 1433  ax-i9 1437  ax-ial 1441  ax-i5r 1442  ax-ext 2036
This theorem depends on definitions:  df-bi 114  df-tru 1260  df-nf 1364  df-sb 1660  df-clab 2041  df-cleq 2047  df-clel 2050  df-nfc 2181  df-v 2574  df-dif 2945  df-in 2949  df-ss 2956  df-ni 6430
This theorem is referenced by:  pion  6436  piord  6437  elni2  6440  mulidpi  6444  ltsopi  6446  pitric  6447  pitri3or  6448  ltdcpi  6449  addclpi  6453  mulclpi  6454  addcompig  6455  addasspig  6456  mulcompig  6457  mulasspig  6458  distrpig  6459  addcanpig  6460  mulcanpig  6461  addnidpig  6462  ltexpi  6463  ltapig  6464  ltmpig  6465  nnppipi  6469  enqdc  6487  archnqq  6543  prarloclemarch2  6545  enq0enq  6557  enq0sym  6558  enq0ref  6559  enq0tr  6560  nqnq0pi  6564  nqnq0  6567  addcmpblnq0  6569  mulcmpblnq0  6570  mulcanenq0ec  6571  addclnq0  6577  nqpnq0nq  6579  nqnq0a  6580  nqnq0m  6581  nq0m0r  6582  nq0a0  6583  nnanq0  6584  distrnq0  6585  mulcomnq0  6586  addassnq0lemcl  6587  addassnq0  6588  nq02m  6591  prarloclemlt  6619  prarloclemn  6625
  Copyright terms: Public domain W3C validator