Theorem zex 12599

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

Syntax hints:   ∈ wcel 2149  Vcvv 3463  ℂcc 11097  ℤcz 12590

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5261  ax-cnex 11155  ax-resscn 11156

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-iota 6493  df-fv 6545  df-ov 7414  df-neg 11443  df-z 12591

This theorem is referenced by:  dfuzi  12686  uzval  12863  uzf  12864  fzval  13536  fzf  13538  climz  15599  climaddc1  15685  climmulc2  15687  climsubc1  15688  climsubc2  15689  climlec2  15709  iseraltlem1  15732  divcnvshft  15908  znnen  16267  lcmfval  16678  lcmf0val  16679  odzval  16850  ex-chn2  18693  mulgfval  19134  mulgfvalALT  19135  odinf  19632  odhash  19643  zaddablx  19941  zringplusg  21572  zringmulr  21575  zringmpg  21589  irinitoringc  21597  pzriprnglem13  21611  pzriprnglem14  21612  zrhval2  21626  zrhpsgnmhm  21702  zfbas  24021  uzrest  24022  tgpmulg2  24219  zdis  24942  sszcld  24943  iscmet3lem3  25417  mbfsup  25791  tayl0  26490  ulmval  26508  ulmpm  26511  ulmf2  26512  dchrptlem2  27394  dchrptlem3  27395  elrgspnlem1  33502  elrgspnlem2  33503  elrgspnlem3  33504  elrgspnlem4  33505  elrgspn  33506  elrgspnsubrunlem1  33507  elrgspnsubrun  33509  esplympl  33901  qqhval  34306  dya2iocuni  34617  eulerpartgbij  34706  eulerpartlemmf  34709  ballotlemfval  34824  reprval  34941  divcnvlin  36123  heibor1lem  38347  aks6d1c6isolem2  42831  mzpclall  43349  mzpf  43358  mzpindd  43368  mzpsubst  43370  mzprename  43371  mzpcompact2lem  43373  diophrw  43381  lzenom  43392  diophin  43394  diophun  43395  eq0rabdioph  43398  eqrabdioph  43399  rabdiophlem1  43419  diophren  43431  hashnzfzclim  44923  uzct  45674  nthrucw  47493  oddiadd  48827  2zrngadd  48896  2zrngmul  48904  zlmodzxzldeplem1  49164  digfval  49261