Theorem zex 12509

Description: The set of integers exists. See also zexALT 12520. (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 12508	. 2 ⊢ ℤ ⊆ ℂ
3	1, 2	ssexi 5269	1 ⊢ ℤ ∈ V

Syntax hints:   ∈ wcel 2114  Vcvv 3442  ℂcc 11036  ℤcz 12500

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 2709  ax-sep 5243  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 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-ov 7371  df-neg 11379  df-z 12501

This theorem is referenced by:  dfuzi  12595  uzval  12765  uzf  12766  fzval  13437  fzf  13439  climz  15484  climaddc1  15570  climmulc2  15572  climsubc1  15573  climsubc2  15574  climlec2  15594  iseraltlem1  15617  divcnvshft  15790  znnen  16149  lcmfval  16560  lcmf0val  16561  odzval  16731  ex-chn2  18573  mulgfval  19011  mulgfvalALT  19012  odinf  19504  odhash  19515  zaddablx  19813  zringplusg  21421  zringmulr  21424  zringmpg  21438  irinitoringc  21446  pzriprnglem13  21460  pzriprnglem14  21461  zrhval2  21475  zrhpsgnmhm  21551  zfbas  23852  uzrest  23853  tgpmulg2  24050  zdis  24773  sszcld  24774  iscmet3lem3  25258  mbfsup  25633  tayl0  26337  ulmval  26357  ulmpm  26360  ulmf2  26361  dchrptlem2  27244  dchrptlem3  27245  elrgspnlem1  33336  elrgspnlem2  33337  elrgspnlem3  33338  elrgspnlem4  33339  elrgspn  33340  elrgspnsubrunlem1  33341  elrgspnsubrun  33343  esplympl  33744  qqhval  34150  dya2iocuni  34461  eulerpartgbij  34550  eulerpartlemmf  34553  ballotlemfval  34668  reprval  34788  divcnvlin  35949  heibor1lem  38060  aks6d1c6isolem2  42545  mzpclall  43084  mzpf  43093  mzpindd  43103  mzpsubst  43105  mzprename  43106  mzpcompact2lem  43108  diophrw  43116  lzenom  43127  diophin  43129  diophun  43130  eq0rabdioph  43133  eqrabdioph  43134  rabdiophlem1  43158  diophren  43170  hashnzfzclim  44678  uzct  45423  nthrucw  47244  oddiadd  48534  2zrngadd  48603  2zrngmul  48611  zlmodzxzldeplem1  48860  digfval  48957