Theorem zex 12742

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

This proof depends on syntax axioms:   ∈ wcel 2147  Vcvv 3454  ℂcc 11237  ℤcz 12733

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255  ax-cnex 11295  ax-resscn 11296

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-iota 6520  df-fv 6574  df-ov 7454  df-neg 11583  df-z 12734

This theorem is used by:  dfuzi  12830  uzval  13007  uzf  13008  fzval  13681  fzf  13683  climz  15760  climaddc1  15846  climmulc2  15848  climsubc1  15849  climsubc2  15850  climlec2  15870  iseraltlem1  15893  divcnvshft  16068  znnen  16424  lcmfval  16840  lcmf0val  16841  odzval  17013  ex-chn2  18862  mulgfval  19329  mulgfvalALT  19330  odinf  19828  odhash  19839  zaddablx  20137  zringplusg  21814  zringeuf  21815  zringmulr  21818  zringmpg  21832  irinitoringc  21840  pzriprnglem13  21854  pzriprnglem14  21855  zrhval2  21869  zrhpsgnmhm  21945  zfbas  24270  uzrest  24271  tgpmulg2  24468  zdis  25191  sszcld  25192  iscmet3lem3  25666  mbfsup  26040  tayl0  26746  ulmval  26764  ulmpm  26767  ulmf2  26768  dchrptlem2  27649  dchrptlem3  27650  elrgspnlem1  33902  elrgspnlem2  33903  elrgspnlem3  33904  elrgspnlem4  33905  elrgspnsubrunlem1  33907  esplympl  34310  qqhval  34715  dya2iocuni  35026  eulerpartgbij  35115  eulerpartlemmf  35118  ballotlemfval  35233  reprval  35350  divcnvlin  36713  heibor1lem  39009  aks6d1c6isolem2  43491  mzpclall  44004  mzpf  44013  mzpindd  44023  mzpsubst  44025  mzprename  44026  mzpcompact2lem  44028  diophrw  44036  lzenom  44047  diophin  44049  diophun  44050  eq0rabdioph  44053  eqrabdioph  44054  rabdiophlem1  44074  diophren  44086  hashnzfzclim  45567  uzct  46354  numtowerdt  48189  oddiadd  49544  2zrngadd  49613  2zrngmul  49621  lazssaz  49730  zlmodzxzldeplem1  49943  digfval  50040