Theorem zex 12709

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

This proof depends on syntax axioms:   ∈ wcel 2144  Vcvv 3450  ℂcc 11205  ℤcz 12700

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-cnex 11263  ax-resscn 11264

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6497  df-fv 6551  df-ov 7427  df-neg 11551  df-z 12701

This theorem is used by:  dfuzi  12797  uzval  12974  uzf  12975  fzval  13648  fzf  13650  climz  15725  climaddc1  15811  climmulc2  15813  climsubc1  15814  climsubc2  15815  climlec2  15835  iseraltlem1  15858  divcnvshft  16033  znnen  16389  lcmfval  16805  lcmf0val  16806  odzval  16978  ex-chn2  18821  mulgfval  19288  mulgfvalALT  19289  odinf  19786  odhash  19797  zaddablx  20095  zringplusg  21769  zringmulr  21772  zringmpg  21786  irinitoringc  21794  pzriprnglem13  21808  pzriprnglem14  21809  zrhval2  21823  zrhpsgnmhm  21899  zfbas  24224  uzrest  24225  tgpmulg2  24422  zdis  25145  sszcld  25146  iscmet3lem3  25620  mbfsup  25994  tayl0  26698  ulmval  26716  ulmpm  26719  ulmf2  26720  dchrptlem2  27601  dchrptlem3  27602  elrgspnlem1  33853  elrgspnlem2  33854  elrgspnlem3  33855  elrgspnlem4  33856  elrgspnsubrunlem1  33858  esplympl  34249  qqhval  34654  dya2iocuni  34965  eulerpartgbij  35054  eulerpartlemmf  35057  ballotlemfval  35172  reprval  35289  divcnvlin  36622  heibor1lem  38880  aks6d1c6isolem2  43362  mzpclall  43875  mzpf  43884  mzpindd  43894  mzpsubst  43896  mzprename  43897  mzpcompact2lem  43899  diophrw  43907  lzenom  43918  diophin  43920  diophun  43921  eq0rabdioph  43924  eqrabdioph  43925  rabdiophlem1  43945  diophren  43957  hashnzfzclim  45443  uzct  46216  numtowerdt  48052  oddiadd  49407  2zrngadd  49476  2zrngmul  49484  zlmodzxzldeplem1  49748  digfval  49845