Theorem zex 12527

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

Syntax hints:   ∈ wcel 2114  Vcvv 3430  ℂcc 11030  ℤcz 12518

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5232  ax-cnex 11088  ax-resscn 11089

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6449  df-fv 6501  df-ov 7364  df-neg 11374  df-z 12519

This theorem is referenced by:  dfuzi  12614  uzval  12784  uzf  12785  fzval  13457  fzf  13459  climz  15505  climaddc1  15591  climmulc2  15593  climsubc1  15594  climsubc2  15595  climlec2  15615  iseraltlem1  15638  divcnvshft  15814  znnen  16173  lcmfval  16584  lcmf0val  16585  odzval  16756  ex-chn2  18598  mulgfval  19039  mulgfvalALT  19040  odinf  19532  odhash  19543  zaddablx  19841  zringplusg  21447  zringmulr  21450  zringmpg  21464  irinitoringc  21472  pzriprnglem13  21486  pzriprnglem14  21487  zrhval2  21501  zrhpsgnmhm  21577  zfbas  23874  uzrest  23875  tgpmulg2  24072  zdis  24795  sszcld  24796  iscmet3lem3  25270  mbfsup  25644  tayl0  26341  ulmval  26361  ulmpm  26364  ulmf2  26365  dchrptlem2  27245  dchrptlem3  27246  elrgspnlem1  33321  elrgspnlem2  33322  elrgspnlem3  33323  elrgspnlem4  33324  elrgspn  33325  elrgspnsubrunlem1  33326  elrgspnsubrun  33328  esplympl  33729  qqhval  34135  dya2iocuni  34446  eulerpartgbij  34535  eulerpartlemmf  34538  ballotlemfval  34653  reprval  34773  divcnvlin  35934  heibor1lem  38147  aks6d1c6isolem2  42631  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  43250  diophren  43262  hashnzfzclim  44770  uzct  45515  nthrucw  47335  oddiadd  48665  2zrngadd  48734  2zrngmul  48742  zlmodzxzldeplem1  48991  digfval  49088