Theorem zex 11263

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

Syntax hints:   ∈ wcel 1977  Vcvv 3173  ℂcc 9813  ℤcz 11254

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-cnex 9871  ax-resscn 9872

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812  df-ov 6552  df-neg 10148  df-z 11255

This theorem is referenced by:  dfuzi  11344  uzval  11565  uzf  11566  fzval  12199  fzf  12201  wrdexg  13170  climz  14128  climaddc1  14213  climmulc2  14215  climsubc1  14216  climsubc2  14217  climlec2  14237  iseraltlem1  14260  divcnvshft  14426  znnen  14780  lcmfval  15172  lcmf0val  15173  odzval  15334  1arithlem1  15465  1arith  15469  mulgfval  17365  odinf  17803  odhash  17812  zaddablx  18098  zringplusg  19644  zringmulr  19646  zringmpg  19659  zrhval2  19676  zrhpsgnmhm  19749  zfbas  21510  uzrest  21511  tgpmulg2  21708  zdis  22427  sszcld  22428  iscmet3lem3  22896  mbfsup  23237  tayl0  23920  ulmval  23938  ulmpm  23941  ulmf2  23942  musum  24717  dchrptlem2  24790  dchrptlem3  24791  qqhval  29346  dya2iocuni  29672  eulerpartgbij  29761  eulerpartlemmf  29764  ballotlemfval  29878  divcnvlin  30871  heibor1lem  32778  mzpclall  36308  mzpf  36317  mzpindd  36327  mzpsubst  36329  mzprename  36330  mzpcompact2lem  36332  diophrw  36340  lzenom  36351  diophin  36354  diophun  36355  eq0rabdioph  36358  eqrabdioph  36359  rabdiophlem1  36383  diophren  36395  hashnzfzclim  37543  uzct  38257  oddiadd  41604  2zrngadd  41727  2zrngmul  41735  irinitoringc  41861  zlmodzxzldeplem1  42083  digfval  42189