Theorem zex 12595

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

Syntax hints:   ∈ wcel 2143  Vcvv 3455  ℂcc 11093  ℤcz 12586

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-cnex 11151  ax-resscn 11152

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-iota 6492  df-fv 6544  df-ov 7413  df-neg 11439  df-z 12587

This theorem is referenced by:  dfuzi  12682  uzval  12859  uzf  12860  fzval  13532  fzf  13534  climz  15596  climaddc1  15682  climmulc2  15684  climsubc1  15685  climsubc2  15686  climlec2  15706  iseraltlem1  15729  divcnvshft  15905  znnen  16263  lcmfval  16674  lcmf0val  16675  odzval  16846  ex-chn2  18689  mulgfval  19130  mulgfvalALT  19131  odinf  19628  odhash  19639  zaddablx  19937  zringplusg  21604  zringmulr  21607  zringmpg  21621  irinitoringc  21629  pzriprnglem13  21643  pzriprnglem14  21644  zrhval2  21658  zrhpsgnmhm  21734  zfbas  24053  uzrest  24054  tgpmulg2  24251  zdis  24974  sszcld  24975  iscmet3lem3  25449  mbfsup  25823  tayl0  26525  ulmval  26543  ulmpm  26546  ulmf2  26547  dchrptlem2  27429  dchrptlem3  27430  elrgspnlem1  33562  elrgspnlem2  33563  elrgspnlem3  33564  elrgspnlem4  33565  elrgspn  33566  elrgspnsubrunlem1  33567  elrgspnsubrun  33569  esplympl  33957  qqhval  34362  dya2iocuni  34673  eulerpartgbij  34762  eulerpartlemmf  34765  ballotlemfval  34880  reprval  34997  divcnvlin  36225  heibor1lem  38460  aks6d1c6isolem2  42942  mzpclall  43458  mzpf  43467  mzpindd  43477  mzpsubst  43479  mzprename  43480  mzpcompact2lem  43482  diophrw  43490  lzenom  43501  diophin  43503  diophun  43504  eq0rabdioph  43507  eqrabdioph  43508  rabdiophlem1  43528  diophren  43540  hashnzfzclim  45032  uzct  45783  nthrucw  47607  oddiadd  48939  2zrngadd  49008  2zrngmul  49016  zlmodzxzldeplem1  49280  digfval  49377