Theorem zex 12564

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

Syntax hints:   ∈ wcel 2098  Vcvv 3466  ℂcc 11104  ℤcz 12555

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695  ax-sep 5289  ax-cnex 11162  ax-resscn 11163

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-rab 3425  df-v 3468  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-nul 4315  df-if 4521  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-br 5139  df-iota 6485  df-fv 6541  df-ov 7404  df-neg 11444  df-z 12556

This theorem is referenced by:  dfuzi  12650  uzval  12821  uzf  12822  fzval  13483  fzf  13485  climz  15490  climaddc1  15576  climmulc2  15578  climsubc1  15579  climsubc2  15580  climlec2  15602  iseraltlem1  15625  divcnvshft  15798  znnen  16152  lcmfval  16555  lcmf0val  16556  odzval  16723  mulgfval  18987  mulgfvalALT  18988  odinf  19473  odhash  19484  zaddablx  19782  zringplusg  21309  zringmulr  21312  zringmpg  21326  irinitoringc  21334  pzriprnglem13  21348  pzriprnglem14  21349  zrhval2  21363  zrhpsgnmhm  21445  zfbas  23722  uzrest  23723  tgpmulg2  23920  zdis  24654  sszcld  24655  iscmet3lem3  25140  mbfsup  25515  tayl0  26215  ulmval  26233  ulmpm  26236  ulmf2  26237  dchrptlem2  27114  dchrptlem3  27115  qqhval  33443  dya2iocuni  33771  eulerpartgbij  33860  eulerpartlemmf  33863  ballotlemfval  33977  reprval  34111  divcnvlin  35197  heibor1lem  37167  mzpclall  41954  mzpf  41963  mzpindd  41973  mzpsubst  41975  mzprename  41976  mzpcompact2lem  41978  diophrw  41986  lzenom  41997  diophin  41999  diophun  42000  eq0rabdioph  42003  eqrabdioph  42004  rabdiophlem1  42028  diophren  42040  hashnzfzclim  43570  uzct  44238  oddiadd  47037  2zrngadd  47106  2zrngmul  47114  zlmodzxzldeplem1  47369  digfval  47471