Theorem zex 12497

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

Syntax hints:   ∈ wcel 2113  Vcvv 3440  ℂcc 11024  ℤcz 12488

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 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-cnex 11082  ax-resscn 11083

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 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361  df-neg 11367  df-z 12489

This theorem is referenced by:  dfuzi  12583  uzval  12753  uzf  12754  fzval  13425  fzf  13427  climz  15472  climaddc1  15558  climmulc2  15560  climsubc1  15561  climsubc2  15562  climlec2  15582  iseraltlem1  15605  divcnvshft  15778  znnen  16137  lcmfval  16548  lcmf0val  16549  odzval  16719  ex-chn2  18561  mulgfval  18999  mulgfvalALT  19000  odinf  19492  odhash  19503  zaddablx  19801  zringplusg  21409  zringmulr  21412  zringmpg  21426  irinitoringc  21434  pzriprnglem13  21448  pzriprnglem14  21449  zrhval2  21463  zrhpsgnmhm  21539  zfbas  23840  uzrest  23841  tgpmulg2  24038  zdis  24761  sszcld  24762  iscmet3lem3  25246  mbfsup  25621  tayl0  26325  ulmval  26345  ulmpm  26348  ulmf2  26349  dchrptlem2  27232  dchrptlem3  27233  elrgspnlem1  33324  elrgspnlem2  33325  elrgspnlem3  33326  elrgspnlem4  33327  elrgspn  33328  elrgspnsubrunlem1  33329  elrgspnsubrun  33331  esplympl  33725  qqhval  34129  dya2iocuni  34440  eulerpartgbij  34529  eulerpartlemmf  34532  ballotlemfval  34647  reprval  34767  divcnvlin  35927  heibor1lem  38010  aks6d1c6isolem2  42429  mzpclall  42969  mzpf  42978  mzpindd  42988  mzpsubst  42990  mzprename  42991  mzpcompact2lem  42993  diophrw  43001  lzenom  43012  diophin  43014  diophun  43015  eq0rabdioph  43018  eqrabdioph  43019  rabdiophlem1  43043  diophren  43055  hashnzfzclim  44563  uzct  45308  nthrucw  47130  oddiadd  48420  2zrngadd  48489  2zrngmul  48497  zlmodzxzldeplem1  48746  digfval  48843