Theorem zex 11424

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

Syntax hints:   ∈ wcel 2030  Vcvv 3231  ℂcc 9972  ℤcz 11415

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-cnex 10030  ax-resscn 10031

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-iota 5889  df-fv 5934  df-ov 6693  df-neg 10307  df-z 11416

This theorem is referenced by:  dfuzi  11506  uzval  11727  uzf  11728  fzval  12366  fzf  12368  wrdexg  13347  climz  14324  climaddc1  14409  climmulc2  14411  climsubc1  14412  climsubc2  14413  climlec2  14433  iseraltlem1  14456  divcnvshft  14631  znnen  14985  lcmfval  15381  lcmf0val  15382  odzval  15543  1arithlem1  15674  1arith  15678  mulgfval  17589  odinf  18026  odhash  18035  zaddablx  18321  zringplusg  19873  zringmulr  19875  zringmpg  19888  zrhval2  19905  zrhpsgnmhm  19978  zfbas  21747  uzrest  21748  tgpmulg2  21945  zdis  22666  sszcld  22667  iscmet3lem3  23134  mbfsup  23476  tayl0  24161  ulmval  24179  ulmpm  24182  ulmf2  24183  musum  24962  dchrptlem2  25035  dchrptlem3  25036  qqhval  30146  dya2iocuni  30473  eulerpartgbij  30562  eulerpartlemmf  30565  ballotlemfval  30679  reprval  30816  divcnvlin  31744  heibor1lem  33738  mzpclall  37607  mzpf  37616  mzpindd  37626  mzpsubst  37628  mzprename  37629  mzpcompact2lem  37631  diophrw  37639  lzenom  37650  diophin  37653  diophun  37654  eq0rabdioph  37657  eqrabdioph  37658  rabdiophlem1  37682  diophren  37694  hashnzfzclim  38838  uzct  39546  oddiadd  42139  2zrngadd  42262  2zrngmul  42270  irinitoringc  42394  zlmodzxzldeplem1  42614  digfval  42716