Theorem zex 12615

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

This proof depends on syntax axioms:   ∈ wcel 2146  Vcvv 3457  ℂcc 11113  ℤcz 12606

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-cnex 11171  ax-resscn 11172

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548  df-ov 7422  df-neg 11459  df-z 12607

This theorem is used by:  dfuzi  12703  uzval  12880  uzf  12881  fzval  13553  fzf  13555  climz  15624  climaddc1  15710  climmulc2  15712  climsubc1  15713  climsubc2  15714  climlec2  15734  iseraltlem1  15757  divcnvshft  15932  znnen  16290  lcmfval  16701  lcmf0val  16702  odzval  16873  ex-chn2  18716  mulgfval  19179  mulgfvalALT  19180  odinf  19677  odhash  19688  zaddablx  19986  zringplusg  21654  zringmulr  21657  zringmpg  21671  irinitoringc  21679  pzriprnglem13  21693  pzriprnglem14  21694  zrhval2  21708  zrhpsgnmhm  21784  zfbas  24104  uzrest  24105  tgpmulg2  24302  zdis  25025  sszcld  25026  iscmet3lem3  25500  mbfsup  25874  tayl0  26576  ulmval  26594  ulmpm  26597  ulmf2  26598  dchrptlem2  27480  dchrptlem3  27481  elrgspnlem1  33626  elrgspnlem2  33627  elrgspnlem3  33628  elrgspnlem4  33629  elrgspn  33630  elrgspnsubrunlem1  33631  elrgspnsubrun  33633  esplympl  34021  qqhval  34426  dya2iocuni  34738  eulerpartgbij  34827  eulerpartlemmf  34830  ballotlemfval  34945  reprval  35062  divcnvlin  36262  heibor1lem  38518  aks6d1c6isolem2  43000  mzpclall  43516  mzpf  43525  mzpindd  43535  mzpsubst  43537  mzprename  43538  mzpcompact2lem  43540  diophrw  43548  lzenom  43559  diophin  43561  diophun  43562  eq0rabdioph  43565  eqrabdioph  43566  rabdiophlem1  43586  diophren  43598  hashnzfzclim  45090  uzct  45841  nthrucw  47665  oddiadd  48996  2zrngadd  49065  2zrngmul  49073  zlmodzxzldeplem1  49337  digfval  49434