Theorem zex 12524

Description: The set of integers exists. See also zexALT 12535. (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 11110	. 2 ⊢ ℂ ∈ V
2		zsscn 12523	. 2 ⊢ ℤ ⊆ ℂ
3	1, 2	ssexi 5250	1 ⊢ ℤ ∈ V

Syntax hints:   ∈ wcel 2119  Vcvv 3431  ℂcc 11027  ℤcz 12515

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-cnex 11085  ax-resscn 11086

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-iota 6441  df-fv 6493  df-ov 7359  df-neg 11371  df-z 12516

This theorem is referenced by:  dfuzi  12611  uzval  12781  uzf  12782  fzval  13454  fzf  13456  climz  15502  climaddc1  15588  climmulc2  15590  climsubc1  15591  climsubc2  15592  climlec2  15612  iseraltlem1  15635  divcnvshft  15811  znnen  16170  lcmfval  16581  lcmf0val  16582  odzval  16753  ex-chn2  18595  mulgfval  19036  mulgfvalALT  19037  odinf  19529  odhash  19540  zaddablx  19838  zringplusg  21429  zringmulr  21432  zringmpg  21446  irinitoringc  21454  pzriprnglem13  21468  pzriprnglem14  21469  zrhval2  21483  zrhpsgnmhm  21559  zfbas  23879  uzrest  23880  tgpmulg2  24077  zdis  24800  sszcld  24801  iscmet3lem3  25275  mbfsup  25649  tayl0  26345  ulmval  26363  ulmpm  26366  ulmf2  26367  dchrptlem2  27246  dchrptlem3  27247  elrgspnlem1  33323  elrgspnlem2  33324  elrgspnlem3  33325  elrgspnlem4  33326  elrgspn  33327  elrgspnsubrunlem1  33328  elrgspnsubrun  33330  esplympl  33751  qqhval  34156  dya2iocuni  34467  eulerpartgbij  34556  eulerpartlemmf  34559  ballotlemfval  34674  reprval  34794  divcnvlin  35961  heibor1lem  38176  aks6d1c6isolem2  42660  mzpclall  43176  mzpf  43185  mzpindd  43195  mzpsubst  43197  mzprename  43198  mzpcompact2lem  43200  diophrw  43208  lzenom  43219  diophin  43221  diophun  43222  eq0rabdioph  43225  eqrabdioph  43226  rabdiophlem1  43246  diophren  43258  hashnzfzclim  44766  uzct  45511  nthrucw  47331  oddiadd  48665  2zrngadd  48734  2zrngmul  48742  zlmodzxzldeplem1  48991  digfval  49088