Theorem nnex 9112

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 8119	. 2 ⊢ ℂ ∈ V
2		nnsscn 9111	. 2 ⊢ ℕ ⊆ ℂ
3	1, 2	ssexi 4221	1 ⊢ ℕ ∈ V

Syntax hints:   ∈ wcel 2200  Vcvv 2799  ℂcc 7993  ℕcn 9106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-sep 4201  ax-cnex 8086  ax-resscn 8087  ax-1re 8089  ax-addrcl 8092

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-v 2801  df-in 3203  df-ss 3210  df-int 3923  df-inn 9107

This theorem is referenced by:  nn0ex  9371  nn0ennn  10650  climrecvg1n  11854  climcvg1nlem  11855  divcnv  12003  trireciplem  12006  expcnvap0  12008  expcnv  12010  geo2lim  12022  prmex  12630  qnumval  12702  qdenval  12703  oddennn  12958  evenennn  12959  xpnnen  12960  znnen  12964  qnnen  12997  ssnnctlemct  13012  nninfdc  13019  ndxarg  13050  mulgnngsum  13659  trilpo  16370  redcwlpo  16382  nconstwlpo  16393  neapmkv  16395