Theorem zex 12477

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

Syntax hints:   ∈ wcel 2111  Vcvv 3436  ℂcc 11004  ℤcz 12468

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5232  ax-cnex 11062  ax-resscn 11063

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-iota 6437  df-fv 6489  df-ov 7349  df-neg 11347  df-z 12469

This theorem is referenced by:  dfuzi  12564  uzval  12734  uzf  12735  fzval  13409  fzf  13411  climz  15456  climaddc1  15542  climmulc2  15544  climsubc1  15545  climsubc2  15546  climlec2  15566  iseraltlem1  15589  divcnvshft  15762  znnen  16121  lcmfval  16532  lcmf0val  16533  odzval  16703  ex-chn2  18544  mulgfval  18982  mulgfvalALT  18983  odinf  19475  odhash  19486  zaddablx  19784  zringplusg  21391  zringmulr  21394  zringmpg  21408  irinitoringc  21416  pzriprnglem13  21430  pzriprnglem14  21431  zrhval2  21445  zrhpsgnmhm  21521  zfbas  23811  uzrest  23812  tgpmulg2  24009  zdis  24732  sszcld  24733  iscmet3lem3  25217  mbfsup  25592  tayl0  26296  ulmval  26316  ulmpm  26319  ulmf2  26320  dchrptlem2  27203  dchrptlem3  27204  elrgspnlem1  33209  elrgspnlem2  33210  elrgspnlem3  33211  elrgspnlem4  33212  elrgspn  33213  elrgspnsubrunlem1  33214  elrgspnsubrun  33216  esplympl  33588  qqhval  33985  dya2iocuni  34296  eulerpartgbij  34385  eulerpartlemmf  34388  ballotlemfval  34503  reprval  34623  divcnvlin  35777  heibor1lem  37857  aks6d1c6isolem2  42216  mzpclall  42768  mzpf  42777  mzpindd  42787  mzpsubst  42789  mzprename  42790  mzpcompact2lem  42792  diophrw  42800  lzenom  42811  diophin  42813  diophun  42814  eq0rabdioph  42817  eqrabdioph  42818  rabdiophlem1  42842  diophren  42854  hashnzfzclim  44363  uzct  45108  oddiadd  48213  2zrngadd  48282  2zrngmul  48290  zlmodzxzldeplem1  48540  digfval  48637