Theorem zex 12577

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

Syntax hints:   ∈ wcel 2142  Vcvv 3454  ℂcc 11071  ℤcz 12568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5246  ax-cnex 11129  ax-resscn 11130

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1099  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6477  df-fv 6529  df-ov 7399  df-neg 11417  df-z 12569

This theorem is referenced by:  dfuzi  12664  uzval  12841  uzf  12842  fzval  13514  fzf  13516  climz  15576  climaddc1  15662  climmulc2  15664  climsubc1  15665  climsubc2  15666  climlec2  15686  iseraltlem1  15709  divcnvshft  15885  znnen  16244  lcmfval  16655  lcmf0val  16656  odzval  16827  ex-chn2  18670  mulgfval  19111  mulgfvalALT  19112  odinf  19603  odhash  19614  zaddablx  19912  zringplusg  21503  zringmulr  21506  zringmpg  21520  irinitoringc  21528  pzriprnglem13  21542  pzriprnglem14  21543  zrhval2  21557  zrhpsgnmhm  21633  zfbas  23953  uzrest  23954  tgpmulg2  24151  zdis  24874  sszcld  24875  iscmet3lem3  25349  mbfsup  25723  tayl0  26422  ulmval  26440  ulmpm  26443  ulmf2  26444  dchrptlem2  27326  dchrptlem3  27327  elrgspnlem1  33420  elrgspnlem2  33421  elrgspnlem3  33422  elrgspnlem4  33423  elrgspn  33424  elrgspnsubrunlem1  33425  elrgspnsubrun  33427  esplympl  33861  qqhval  34266  dya2iocuni  34577  eulerpartgbij  34666  eulerpartlemmf  34669  ballotlemfval  34784  reprval  34901  divcnvlin  36080  heibor1lem  38305  aks6d1c6isolem2  42789  mzpclall  43305  mzpf  43314  mzpindd  43324  mzpsubst  43326  mzprename  43327  mzpcompact2lem  43329  diophrw  43337  lzenom  43348  diophin  43350  diophun  43351  eq0rabdioph  43354  eqrabdioph  43355  rabdiophlem1  43375  diophren  43387  hashnzfzclim  44895  uzct  45640  nthrucw  47459  oddiadd  48793  2zrngadd  48862  2zrngmul  48870  zlmodzxzldeplem1  49119  digfval  49216