Theorem zex 11993

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

Syntax hints:   ∈ wcel 2114  Vcvv 3496  ℂcc 10537  ℤcz 11984

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-cnex 10595  ax-resscn 10596

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-iota 6316  df-fv 6365  df-ov 7161  df-neg 10875  df-z 11985

This theorem is referenced by:  dfuzi  12076  uzval  12248  uzf  12249  fzval  12897  fzf  12899  wrdexgOLD  13875  climz  14908  climaddc1  14993  climmulc2  14995  climsubc1  14996  climsubc2  14997  climlec2  15017  iseraltlem1  15040  divcnvshft  15212  znnen  15567  lcmfval  15967  lcmf0val  15968  odzval  16130  mulgfval  18228  mulgfvalALT  18229  odinf  18692  odhash  18701  zaddablx  18994  zringplusg  20626  zringmulr  20628  zringmpg  20641  zrhval2  20658  zrhpsgnmhm  20730  zfbas  22506  uzrest  22507  tgpmulg2  22704  zdis  23426  sszcld  23427  iscmet3lem3  23895  mbfsup  24267  tayl0  24952  ulmval  24970  ulmpm  24973  ulmf2  24974  dchrptlem2  25843  dchrptlem3  25844  qqhval  31217  dya2iocuni  31543  eulerpartgbij  31632  eulerpartlemmf  31635  ballotlemfval  31749  reprval  31883  divcnvlin  32966  heibor1lem  35089  mzpclall  39331  mzpf  39340  mzpindd  39350  mzpsubst  39352  mzprename  39353  mzpcompact2lem  39355  diophrw  39363  lzenom  39374  diophin  39376  diophun  39377  eq0rabdioph  39380  eqrabdioph  39381  rabdiophlem1  39405  diophren  39417  hashnzfzclim  40661  uzct  41332  oddiadd  44088  2zrngadd  44215  2zrngmul  44223  irinitoringc  44347  zlmodzxzldeplem1  44562  digfval  44664