Theorem zex 12563

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

Syntax hints:   ∈ wcel 2106  Vcvv 3474  ℂcc 11104  ℤcz 12554

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5298  ax-cnex 11162  ax-resscn 11163

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-iota 6492  df-fv 6548  df-ov 7408  df-neg 11443  df-z 12555

This theorem is referenced by:  dfuzi  12649  uzval  12820  uzf  12821  fzval  13482  fzf  13484  climz  15489  climaddc1  15575  climmulc2  15577  climsubc1  15578  climsubc2  15579  climlec2  15601  iseraltlem1  15624  divcnvshft  15797  znnen  16151  lcmfval  16554  lcmf0val  16555  odzval  16720  mulgfval  18946  mulgfvalALT  18947  odinf  19425  odhash  19436  zaddablx  19734  zringplusg  21016  zringmulr  21018  zringmpg  21032  zrhval2  21049  zrhpsgnmhm  21128  zfbas  23391  uzrest  23392  tgpmulg2  23589  zdis  24323  sszcld  24324  iscmet3lem3  24798  mbfsup  25172  tayl0  25865  ulmval  25883  ulmpm  25886  ulmf2  25887  dchrptlem2  26757  dchrptlem3  26758  qqhval  32942  dya2iocuni  33270  eulerpartgbij  33359  eulerpartlemmf  33362  ballotlemfval  33476  reprval  33610  divcnvlin  34690  heibor1lem  36665  mzpclall  41450  mzpf  41459  mzpindd  41469  mzpsubst  41471  mzprename  41472  mzpcompact2lem  41474  diophrw  41482  lzenom  41493  diophin  41495  diophun  41496  eq0rabdioph  41499  eqrabdioph  41500  rabdiophlem1  41524  diophren  41536  hashnzfzclim  43066  uzct  43735  oddiadd  46570  2zrngadd  46788  2zrngmul  46796  irinitoringc  46920  zlmodzxzldeplem1  47134  digfval  47236