Theorem zex 12605

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

Syntax hints:   ∈ wcel 2107  Vcvv 3463  ℂcc 11135  ℤcz 12596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706  ax-sep 5276  ax-cnex 11193  ax-resscn 11194

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-rab 3420  df-v 3465  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-br 5124  df-iota 6494  df-fv 6549  df-ov 7416  df-neg 11477  df-z 12597

This theorem is referenced by:  dfuzi  12692  uzval  12862  uzf  12863  fzval  13531  fzf  13533  climz  15567  climaddc1  15653  climmulc2  15655  climsubc1  15656  climsubc2  15657  climlec2  15677  iseraltlem1  15700  divcnvshft  15873  znnen  16230  lcmfval  16640  lcmf0val  16641  odzval  16811  mulgfval  19056  mulgfvalALT  19057  odinf  19549  odhash  19560  zaddablx  19858  zringplusg  21427  zringmulr  21430  zringmpg  21444  irinitoringc  21452  pzriprnglem13  21466  pzriprnglem14  21467  zrhval2  21481  zrhpsgnmhm  21556  zfbas  23850  uzrest  23851  tgpmulg2  24048  zdis  24774  sszcld  24775  iscmet3lem3  25260  mbfsup  25635  tayl0  26339  ulmval  26359  ulmpm  26362  ulmf2  26363  dchrptlem2  27245  dchrptlem3  27246  elrgspnlem1  33185  elrgspnlem2  33186  elrgspnlem3  33187  elrgspnlem4  33188  elrgspn  33189  elrgspnsubrunlem1  33190  elrgspnsubrun  33192  qqhval  33932  dya2iocuni  34244  eulerpartgbij  34333  eulerpartlemmf  34336  ballotlemfval  34451  reprval  34584  divcnvlin  35692  heibor1lem  37775  aks6d1c6isolem2  42135  mzpclall  42701  mzpf  42710  mzpindd  42720  mzpsubst  42722  mzprename  42723  mzpcompact2lem  42725  diophrw  42733  lzenom  42744  diophin  42746  diophun  42747  eq0rabdioph  42750  eqrabdioph  42751  rabdiophlem1  42775  diophren  42787  hashnzfzclim  44298  uzct  45025  oddiadd  48048  2zrngadd  48117  2zrngmul  48125  zlmodzxzldeplem1  48375  digfval  48476