Theorem zex 12533

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

Syntax hints:   ∈ wcel 2114  Vcvv 3429  ℂcc 11036  ℤcz 12524

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 2708  ax-sep 5231  ax-cnex 11094  ax-resscn 11095

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 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370  df-neg 11380  df-z 12525

This theorem is referenced by:  dfuzi  12620  uzval  12790  uzf  12791  fzval  13463  fzf  13465  climz  15511  climaddc1  15597  climmulc2  15599  climsubc1  15600  climsubc2  15601  climlec2  15621  iseraltlem1  15644  divcnvshft  15820  znnen  16179  lcmfval  16590  lcmf0val  16591  odzval  16762  ex-chn2  18604  mulgfval  19045  mulgfvalALT  19046  odinf  19538  odhash  19549  zaddablx  19847  zringplusg  21434  zringmulr  21437  zringmpg  21451  irinitoringc  21459  pzriprnglem13  21473  pzriprnglem14  21474  zrhval2  21488  zrhpsgnmhm  21564  zfbas  23861  uzrest  23862  tgpmulg2  24059  zdis  24782  sszcld  24783  iscmet3lem3  25257  mbfsup  25631  tayl0  26327  ulmval  26345  ulmpm  26348  ulmf2  26349  dchrptlem2  27228  dchrptlem3  27229  elrgspnlem1  33303  elrgspnlem2  33304  elrgspnlem3  33305  elrgspnlem4  33306  elrgspn  33307  elrgspnsubrunlem1  33308  elrgspnsubrun  33310  esplympl  33711  qqhval  34116  dya2iocuni  34427  eulerpartgbij  34516  eulerpartlemmf  34519  ballotlemfval  34634  reprval  34754  divcnvlin  35915  heibor1lem  38130  aks6d1c6isolem2  42614  mzpclall  43159  mzpf  43168  mzpindd  43178  mzpsubst  43180  mzprename  43181  mzpcompact2lem  43183  diophrw  43191  lzenom  43202  diophin  43204  diophun  43205  eq0rabdioph  43208  eqrabdioph  43209  rabdiophlem1  43229  diophren  43241  hashnzfzclim  44749  uzct  45494  nthrucw  47316  oddiadd  48650  2zrngadd  48719  2zrngmul  48727  zlmodzxzldeplem1  48976  digfval  49073