Theorem zex 11737

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

Syntax hints:   ∈ wcel 2106  Vcvv 3397  ℂcc 10270  ℤcz 11728

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-13 2333  ax-ext 2753  ax-sep 5017  ax-cnex 10328  ax-resscn 10329

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-rex 3095  df-rab 3098  df-v 3399  df-dif 3794  df-un 3796  df-in 3798  df-ss 3805  df-nul 4141  df-if 4307  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4672  df-br 4887  df-iota 6099  df-fv 6143  df-ov 6925  df-neg 10609  df-z 11729

This theorem is referenced by:  dfuzi  11820  uzval  11994  uzf  11995  fzval  12645  fzf  12647  wrdexgOLD  13610  climz  14688  climaddc1  14773  climmulc2  14775  climsubc1  14776  climsubc2  14777  climlec2  14797  iseraltlem1  14820  divcnvshft  14991  znnen  15345  lcmfval  15740  lcmf0val  15741  odzval  15900  mulgfval  17929  odinf  18364  odhash  18373  zaddablx  18661  zringplusg  20221  zringmulr  20223  zringmpg  20236  zrhval2  20253  zrhpsgnmhm  20325  zfbas  22108  uzrest  22109  tgpmulg2  22306  zdis  23027  sszcld  23028  iscmet3lem3  23496  mbfsup  23868  tayl0  24553  ulmval  24571  ulmpm  24574  ulmf2  24575  musum  25369  dchrptlem2  25442  dchrptlem3  25443  qqhval  30616  dya2iocuni  30943  eulerpartgbij  31032  eulerpartlemmf  31035  ballotlemfval  31150  reprval  31290  divcnvlin  32212  heibor1lem  34227  mzpclall  38243  mzpf  38252  mzpindd  38262  mzpsubst  38264  mzprename  38265  mzpcompact2lem  38267  diophrw  38275  lzenom  38286  diophin  38289  diophun  38290  eq0rabdioph  38293  eqrabdioph  38294  rabdiophlem1  38318  diophren  38330  hashnzfzclim  39470  uzct  40156  oddiadd  42822  2zrngadd  42945  2zrngmul  42953  irinitoringc  43077  zlmodzxzldeplem1  43297  digfval  43399