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

Theorem nnex 8694
Description: The set of positive integers exists. (Contributed by NM, 3-Oct-1999.) (Revised by Mario Carneiro, 17-Nov-2014.)
Assertion
Ref Expression
nnex ℕ ∈ V

Proof of Theorem nnex
StepHypRef Expression
1 cnex 7712 . 2 ℂ ∈ V
2 nnsscn 8693 . 2 ℕ ⊆ ℂ
31, 2ssexi 4036 1 ℕ ∈ V
Colors of variables: wff set class
Syntax hints:  wcel 1465  Vcvv 2660  cc 7586  cn 8688
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-io 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099  ax-sep 4016  ax-cnex 7679  ax-resscn 7680  ax-1re 7682  ax-addrcl 7685
This theorem depends on definitions:  df-bi 116  df-tru 1319  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-ral 2398  df-v 2662  df-in 3047  df-ss 3054  df-int 3742  df-inn 8689
This theorem is referenced by:  nn0ex  8951  nn0ennn  10174  climrecvg1n  11085  climcvg1nlem  11086  divcnv  11234  trireciplem  11237  expcnvap0  11239  expcnv  11241  geo2lim  11253  prmex  11721  qnumval  11790  qdenval  11791  oddennn  11832  evenennn  11833  xpnnen  11834  znnen  11838  qnnen  11871  ndxarg  11909  trilpo  13163
  Copyright terms: Public domain W3C validator