Theorem zex 12258

Description: The set of integers exists. See also zexALT 12269. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 17-Nov-2014.)

Assertion

Ref	Expression
zex	⊢ ℤ ∈ V

Proof of Theorem zex

Step	Hyp	Ref	Expression
1		cnex 10883	. 2 ⊢ ℂ ∈ V
2		zsscn 12257	. 2 ⊢ ℤ ⊆ ℂ
3	1, 2	ssexi 5241	1 ⊢ ℤ ∈ V

Syntax hints:   ∈ wcel 2108  Vcvv 3422  ℂcc 10800  ℤcz 12249

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-cnex 10858  ax-resscn 10859

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-iota 6376  df-fv 6426  df-ov 7258  df-neg 11138  df-z 12250

This theorem is referenced by:  dfuzi  12341  uzval  12513  uzf  12514  fzval  13170  fzf  13172  climz  15186  climaddc1  15272  climmulc2  15274  climsubc1  15275  climsubc2  15276  climlec2  15298  iseraltlem1  15321  divcnvshft  15495  znnen  15849  lcmfval  16254  lcmf0val  16255  odzval  16420  mulgfval  18617  mulgfvalALT  18618  odinf  19085  odhash  19094  zaddablx  19388  zringplusg  20589  zringmulr  20591  zringmpg  20605  zrhval2  20622  zrhpsgnmhm  20701  zfbas  22955  uzrest  22956  tgpmulg2  23153  zdis  23885  sszcld  23886  iscmet3lem3  24359  mbfsup  24733  tayl0  25426  ulmval  25444  ulmpm  25447  ulmf2  25448  dchrptlem2  26318  dchrptlem3  26319  qqhval  31824  dya2iocuni  32150  eulerpartgbij  32239  eulerpartlemmf  32242  ballotlemfval  32356  reprval  32490  divcnvlin  33604  heibor1lem  35894  mzpclall  40465  mzpf  40474  mzpindd  40484  mzpsubst  40486  mzprename  40487  mzpcompact2lem  40489  diophrw  40497  lzenom  40508  diophin  40510  diophun  40511  eq0rabdioph  40514  eqrabdioph  40515  rabdiophlem1  40539  diophren  40551  hashnzfzclim  41829  uzct  42500  oddiadd  45256  2zrngadd  45383  2zrngmul  45391  irinitoringc  45515  zlmodzxzldeplem1  45729  digfval  45831