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

Theorem pinn 6805
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 6800 . . 3 N = (ω ∖ {∅})
2 difss 3115 . . 3 (ω ∖ {∅}) ⊆ ω
31, 2eqsstri 3045 . 2 N ⊆ ω
43sseli 3010 1 (𝐴N𝐴 ∈ ω)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1436  cdif 2985  c0 3275  {csn 3431  ωcom 4377  Ncnpi 6768
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-v 2617  df-dif 2990  df-in 2994  df-ss 3001  df-ni 6800
This theorem is referenced by:  pion  6806  piord  6807  elni2  6810  mulidpi  6814  ltsopi  6816  pitric  6817  pitri3or  6818  ltdcpi  6819  addclpi  6823  mulclpi  6824  addcompig  6825  addasspig  6826  mulcompig  6827  mulasspig  6828  distrpig  6829  addcanpig  6830  mulcanpig  6831  addnidpig  6832  ltexpi  6833  ltapig  6834  ltmpig  6835  nnppipi  6839  enqdc  6857  archnqq  6913  prarloclemarch2  6915  enq0enq  6927  enq0sym  6928  enq0ref  6929  enq0tr  6930  nqnq0pi  6934  nqnq0  6937  addcmpblnq0  6939  mulcmpblnq0  6940  mulcanenq0ec  6941  addclnq0  6947  nqpnq0nq  6949  nqnq0a  6950  nqnq0m  6951  nq0m0r  6952  nq0a0  6953  nnanq0  6954  distrnq0  6955  mulcomnq0  6956  addassnq0lemcl  6957  addassnq0  6958  nq02m  6961  prarloclemlt  6989  prarloclemn  6995
  Copyright terms: Public domain W3C validator