Theorem zex 12071

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

Syntax hints:   ∈ wcel 2114  Vcvv 3398  ℂcc 10613  ℤcz 12062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2710  ax-sep 5167  ax-cnex 10671  ax-resscn 10672

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-rab 3062  df-v 3400  df-un 3848  df-in 3850  df-ss 3860  df-sn 4517  df-pr 4519  df-op 4523  df-uni 4797  df-br 5031  df-iota 6297  df-fv 6347  df-ov 7173  df-neg 10951  df-z 12063

This theorem is referenced by:  dfuzi  12154  uzval  12326  uzf  12327  fzval  12983  fzf  12985  climz  14996  climaddc1  15082  climmulc2  15084  climsubc1  15085  climsubc2  15086  climlec2  15108  iseraltlem1  15131  divcnvshft  15303  znnen  15657  lcmfval  16062  lcmf0val  16063  odzval  16228  mulgfval  18344  mulgfvalALT  18345  odinf  18808  odhash  18817  zaddablx  19111  zringplusg  20296  zringmulr  20298  zringmpg  20312  zrhval2  20329  zrhpsgnmhm  20400  zfbas  22647  uzrest  22648  tgpmulg2  22845  zdis  23568  sszcld  23569  iscmet3lem3  24042  mbfsup  24416  tayl0  25109  ulmval  25127  ulmpm  25130  ulmf2  25131  dchrptlem2  26001  dchrptlem3  26002  qqhval  31494  dya2iocuni  31820  eulerpartgbij  31909  eulerpartlemmf  31912  ballotlemfval  32026  reprval  32160  divcnvlin  33269  heibor1lem  35590  mzpclall  40121  mzpf  40130  mzpindd  40140  mzpsubst  40142  mzprename  40143  mzpcompact2lem  40145  diophrw  40153  lzenom  40164  diophin  40166  diophun  40167  eq0rabdioph  40170  eqrabdioph  40171  rabdiophlem1  40195  diophren  40207  hashnzfzclim  41478  uzct  42149  oddiadd  44902  2zrngadd  45029  2zrngmul  45037  irinitoringc  45161  zlmodzxzldeplem1  45375  digfval  45477