Theorem zex 12625

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

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3450  ℂcc 11123  ℤcz 12616

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5251  ax-cnex 11181  ax-resscn 11182

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6489  df-fv 6541  df-ov 7417  df-neg 11469  df-z 12617

This theorem is used by:  dfuzi  12713  uzval  12890  uzf  12891  fzval  13564  fzf  13566  climz  15637  climaddc1  15723  climmulc2  15725  climsubc1  15726  climsubc2  15727  climlec2  15747  iseraltlem1  15770  divcnvshft  15945  znnen  16301  lcmfval  16712  lcmf0val  16713  odzval  16884  ex-chn2  18727  mulgfval  19193  mulgfvalALT  19194  odinf  19691  odhash  19702  zaddablx  20000  zringplusg  21668  zringmulr  21671  zringmpg  21685  irinitoringc  21693  pzriprnglem13  21707  pzriprnglem14  21708  zrhval2  21722  zrhpsgnmhm  21798  zfbas  24123  uzrest  24124  tgpmulg2  24321  zdis  25044  sszcld  25045  iscmet3lem3  25519  mbfsup  25893  tayl0  26599  ulmval  26617  ulmpm  26620  ulmf2  26621  dchrptlem2  27502  dchrptlem3  27503  elrgspnlem1  33683  elrgspnlem2  33684  elrgspnlem3  33685  elrgspnlem4  33686  elrgspnsubrunlem1  33688  esplympl  34078  qqhval  34483  dya2iocuni  34795  eulerpartgbij  34884  eulerpartlemmf  34887  ballotlemfval  35002  reprval  35119  divcnvlin  36313  heibor1lem  38560  aks6d1c6isolem2  43042  mzpclall  43573  mzpf  43582  mzpindd  43592  mzpsubst  43594  mzprename  43595  mzpcompact2lem  43597  diophrw  43605  lzenom  43616  diophin  43618  diophun  43619  eq0rabdioph  43622  eqrabdioph  43623  rabdiophlem1  43643  diophren  43655  hashnzfzclim  45147  uzct  45898  numtowerdt  47735  oddiadd  49090  2zrngadd  49159  2zrngmul  49167  zlmodzxzldeplem1  49431  digfval  49528