Theorem zex 12495

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

Syntax hints:   ∈ wcel 2113  Vcvv 3438  ℂcc 11022  ℤcz 12486

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-sep 5239  ax-cnex 11080  ax-resscn 11081

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-iota 6446  df-fv 6498  df-ov 7359  df-neg 11365  df-z 12487

This theorem is referenced by:  dfuzi  12581  uzval  12751  uzf  12752  fzval  13423  fzf  13425  climz  15470  climaddc1  15556  climmulc2  15558  climsubc1  15559  climsubc2  15560  climlec2  15580  iseraltlem1  15603  divcnvshft  15776  znnen  16135  lcmfval  16546  lcmf0val  16547  odzval  16717  ex-chn2  18559  mulgfval  18997  mulgfvalALT  18998  odinf  19490  odhash  19501  zaddablx  19799  zringplusg  21407  zringmulr  21410  zringmpg  21424  irinitoringc  21432  pzriprnglem13  21446  pzriprnglem14  21447  zrhval2  21461  zrhpsgnmhm  21537  zfbas  23838  uzrest  23839  tgpmulg2  24036  zdis  24759  sszcld  24760  iscmet3lem3  25244  mbfsup  25619  tayl0  26323  ulmval  26343  ulmpm  26346  ulmf2  26347  dchrptlem2  27230  dchrptlem3  27231  elrgspnlem1  33273  elrgspnlem2  33274  elrgspnlem3  33275  elrgspnlem4  33276  elrgspn  33277  elrgspnsubrunlem1  33278  elrgspnsubrun  33280  esplympl  33674  qqhval  34078  dya2iocuni  34389  eulerpartgbij  34478  eulerpartlemmf  34481  ballotlemfval  34596  reprval  34716  divcnvlin  35876  heibor1lem  37949  aks6d1c6isolem2  42368  mzpclall  42911  mzpf  42920  mzpindd  42930  mzpsubst  42932  mzprename  42933  mzpcompact2lem  42935  diophrw  42943  lzenom  42954  diophin  42956  diophun  42957  eq0rabdioph  42960  eqrabdioph  42961  rabdiophlem1  42985  diophren  42997  hashnzfzclim  44505  uzct  45250  nthrucw  47072  oddiadd  48362  2zrngadd  48431  2zrngmul  48439  zlmodzxzldeplem1  48688  digfval  48785