Theorem zex 12702

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

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3451  ℂcc 11198  ℤcz 12693

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 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-cnex 11256  ax-resscn 11257

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 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6494  df-fv 6546  df-ov 7423  df-neg 11544  df-z 12694

This theorem is used by:  dfuzi  12790  uzval  12967  uzf  12968  fzval  13641  fzf  13643  climz  15716  climaddc1  15802  climmulc2  15804  climsubc1  15805  climsubc2  15806  climlec2  15826  iseraltlem1  15849  divcnvshft  16024  znnen  16380  lcmfval  16796  lcmf0val  16797  odzval  16969  ex-chn2  18812  mulgfval  19279  mulgfvalALT  19280  odinf  19777  odhash  19788  zaddablx  20086  zringplusg  21760  zringmulr  21763  zringmpg  21777  irinitoringc  21785  pzriprnglem13  21799  pzriprnglem14  21800  zrhval2  21814  zrhpsgnmhm  21890  zfbas  24215  uzrest  24216  tgpmulg2  24413  zdis  25136  sszcld  25137  iscmet3lem3  25611  mbfsup  25985  tayl0  26689  ulmval  26707  ulmpm  26710  ulmf2  26711  dchrptlem2  27592  dchrptlem3  27593  elrgspnlem1  33803  elrgspnlem2  33804  elrgspnlem3  33805  elrgspnlem4  33806  elrgspnsubrunlem1  33808  esplympl  34199  qqhval  34604  dya2iocuni  34915  eulerpartgbij  35004  eulerpartlemmf  35007  ballotlemfval  35122  reprval  35239  divcnvlin  36498  heibor1lem  38743  aks6d1c6isolem2  43225  mzpclall  43737  mzpf  43746  mzpindd  43756  mzpsubst  43758  mzprename  43759  mzpcompact2lem  43761  diophrw  43769  lzenom  43780  diophin  43782  diophun  43783  eq0rabdioph  43786  eqrabdioph  43787  rabdiophlem1  43807  diophren  43819  hashnzfzclim  45305  uzct  46079  numtowerdt  47915  oddiadd  49270  2zrngadd  49339  2zrngmul  49347  zlmodzxzldeplem1  49611  digfval  49708