Theorem zex 12514

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

Syntax hints:   ∈ wcel 2109  Vcvv 3444  ℂcc 11042  ℤcz 12505

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-cnex 11100  ax-resscn 11101

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507  df-ov 7372  df-neg 11384  df-z 12506

This theorem is referenced by:  dfuzi  12601  uzval  12771  uzf  12772  fzval  13446  fzf  13448  climz  15491  climaddc1  15577  climmulc2  15579  climsubc1  15580  climsubc2  15581  climlec2  15601  iseraltlem1  15624  divcnvshft  15797  znnen  16156  lcmfval  16567  lcmf0val  16568  odzval  16738  mulgfval  18977  mulgfvalALT  18978  odinf  19469  odhash  19480  zaddablx  19778  zringplusg  21340  zringmulr  21343  zringmpg  21357  irinitoringc  21365  pzriprnglem13  21379  pzriprnglem14  21380  zrhval2  21394  zrhpsgnmhm  21469  zfbas  23759  uzrest  23760  tgpmulg2  23957  zdis  24681  sszcld  24682  iscmet3lem3  25166  mbfsup  25541  tayl0  26245  ulmval  26265  ulmpm  26268  ulmf2  26269  dchrptlem2  27152  dchrptlem3  27153  elrgspnlem1  33166  elrgspnlem2  33167  elrgspnlem3  33168  elrgspnlem4  33169  elrgspn  33170  elrgspnsubrunlem1  33171  elrgspnsubrun  33173  qqhval  33935  dya2iocuni  34247  eulerpartgbij  34336  eulerpartlemmf  34339  ballotlemfval  34454  reprval  34574  divcnvlin  35693  heibor1lem  37776  aks6d1c6isolem2  42136  mzpclall  42688  mzpf  42697  mzpindd  42707  mzpsubst  42709  mzprename  42710  mzpcompact2lem  42712  diophrw  42720  lzenom  42731  diophin  42733  diophun  42734  eq0rabdioph  42737  eqrabdioph  42738  rabdiophlem1  42762  diophren  42774  hashnzfzclim  44284  uzct  45030  oddiadd  48135  2zrngadd  48204  2zrngmul  48212  zlmodzxzldeplem1  48462  digfval  48559