Theorem nnex 8884

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

Step	Hyp	Ref	Expression
1		cnex 7898	. 2 ⊢ ℂ ∈ V
2		nnsscn 8883	. 2 ⊢ ℕ ⊆ ℂ
3	1, 2	ssexi 4127	1 ⊢ ℕ ∈ V

Syntax hints:   ∈ wcel 2141  Vcvv 2730  ℂcc 7772  ℕcn 8878

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 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152  ax-sep 4107  ax-cnex 7865  ax-resscn 7866  ax-1re 7868  ax-addrcl 7871

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ral 2453  df-v 2732  df-in 3127  df-ss 3134  df-int 3832  df-inn 8879

This theorem is referenced by:  nn0ex  9141  nn0ennn  10389  climrecvg1n  11311  climcvg1nlem  11312  divcnv  11460  trireciplem  11463  expcnvap0  11465  expcnv  11467  geo2lim  11479  prmex  12067  qnumval  12139  qdenval  12140  oddennn  12347  evenennn  12348  xpnnen  12349  znnen  12353  qnnen  12386  ssnnctlemct  12401  nninfdc  12408  ndxarg  12439  trilpo  14075  redcwlpo  14087  nconstwlpo  14097  neapmkv  14099