Theorem zex 12620

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

Syntax hints:   ∈ wcel 2106  Vcvv 3478  ℂcc 11151  ℤcz 12611

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302  ax-cnex 11209  ax-resscn 11210

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-iota 6516  df-fv 6571  df-ov 7434  df-neg 11493  df-z 12612

This theorem is referenced by:  dfuzi  12707  uzval  12878  uzf  12879  fzval  13546  fzf  13548  climz  15582  climaddc1  15668  climmulc2  15670  climsubc1  15671  climsubc2  15672  climlec2  15692  iseraltlem1  15715  divcnvshft  15888  znnen  16245  lcmfval  16655  lcmf0val  16656  odzval  16825  mulgfval  19100  mulgfvalALT  19101  odinf  19596  odhash  19607  zaddablx  19905  zringplusg  21483  zringmulr  21486  zringmpg  21500  irinitoringc  21508  pzriprnglem13  21522  pzriprnglem14  21523  zrhval2  21537  zrhpsgnmhm  21620  zfbas  23920  uzrest  23921  tgpmulg2  24118  zdis  24852  sszcld  24853  iscmet3lem3  25338  mbfsup  25713  tayl0  26418  ulmval  26438  ulmpm  26441  ulmf2  26442  dchrptlem2  27324  dchrptlem3  27325  elrgspnlem1  33232  elrgspnlem2  33233  elrgspnlem3  33234  elrgspnlem4  33235  qqhval  33935  dya2iocuni  34265  eulerpartgbij  34354  eulerpartlemmf  34357  ballotlemfval  34471  reprval  34604  divcnvlin  35713  heibor1lem  37796  aks6d1c6isolem2  42157  mzpclall  42715  mzpf  42724  mzpindd  42734  mzpsubst  42736  mzprename  42737  mzpcompact2lem  42739  diophrw  42747  lzenom  42758  diophin  42760  diophun  42761  eq0rabdioph  42764  eqrabdioph  42765  rabdiophlem1  42789  diophren  42801  hashnzfzclim  44318  uzct  45003  oddiadd  48018  2zrngadd  48087  2zrngmul  48095  zlmodzxzldeplem1  48346  digfval  48447