Theorem nnex 9139

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 8146	. 2 ⊢ ℂ ∈ V
2		nnsscn 9138	. 2 ⊢ ℕ ⊆ ℂ
3	1, 2	ssexi 4225	1 ⊢ ℕ ∈ V

Syntax hints:   ∈ wcel 2200  Vcvv 2800  ℂcc 8020  ℕcn 9133

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 4205  ax-cnex 8113  ax-resscn 8114  ax-1re 8116  ax-addrcl 8119

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 2802  df-in 3204  df-ss 3211  df-int 3927  df-inn 9134

This theorem is referenced by:  nn0ex  9398  nn0ennn  10685  climrecvg1n  11899  climcvg1nlem  11900  divcnv  12048  trireciplem  12051  expcnvap0  12053  expcnv  12055  geo2lim  12067  prmex  12675  qnumval  12747  qdenval  12748  oddennn  13003  evenennn  13004  xpnnen  13005  znnen  13009  qnnen  13042  ssnnctlemct  13057  nninfdc  13064  ndxarg  13095  mulgnngsum  13704  trilpo  16583  redcwlpo  16595  nconstwlpo  16606  neapmkv  16608