Theorem zex 11978

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

Syntax hints:   ∈ wcel 2111  Vcvv 3441  ℂcc 10524  ℤcz 11969

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-cnex 10582  ax-resscn 10583

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-rab 3115  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332  df-ov 7138  df-neg 10862  df-z 11970

This theorem is referenced by:  dfuzi  12061  uzval  12233  uzf  12234  fzval  12887  fzf  12889  climz  14898  climaddc1  14983  climmulc2  14985  climsubc1  14986  climsubc2  14987  climlec2  15007  iseraltlem1  15030  divcnvshft  15202  znnen  15557  lcmfval  15955  lcmf0val  15956  odzval  16118  mulgfval  18218  mulgfvalALT  18219  odinf  18682  odhash  18691  zaddablx  18985  zringplusg  20170  zringmulr  20172  zringmpg  20185  zrhval2  20202  zrhpsgnmhm  20273  zfbas  22501  uzrest  22502  tgpmulg2  22699  zdis  23421  sszcld  23422  iscmet3lem3  23894  mbfsup  24268  tayl0  24957  ulmval  24975  ulmpm  24978  ulmf2  24979  dchrptlem2  25849  dchrptlem3  25850  qqhval  31325  dya2iocuni  31651  eulerpartgbij  31740  eulerpartlemmf  31743  ballotlemfval  31857  reprval  31991  divcnvlin  33077  heibor1lem  35247  mzpclall  39668  mzpf  39677  mzpindd  39687  mzpsubst  39689  mzprename  39690  mzpcompact2lem  39692  diophrw  39700  lzenom  39711  diophin  39713  diophun  39714  eq0rabdioph  39717  eqrabdioph  39718  rabdiophlem1  39742  diophren  39754  hashnzfzclim  41026  uzct  41697  oddiadd  44434  2zrngadd  44561  2zrngmul  44569  irinitoringc  44693  zlmodzxzldeplem1  44909  digfval  45011