Theorem zex 12545

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

Syntax hints:   ∈ wcel 2109  Vcvv 3450  ℂcc 11073  ℤcz 12536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254  ax-cnex 11131  ax-resscn 11132

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393  df-neg 11415  df-z 12537

This theorem is referenced by:  dfuzi  12632  uzval  12802  uzf  12803  fzval  13477  fzf  13479  climz  15522  climaddc1  15608  climmulc2  15610  climsubc1  15611  climsubc2  15612  climlec2  15632  iseraltlem1  15655  divcnvshft  15828  znnen  16187  lcmfval  16598  lcmf0val  16599  odzval  16769  mulgfval  19008  mulgfvalALT  19009  odinf  19500  odhash  19511  zaddablx  19809  zringplusg  21371  zringmulr  21374  zringmpg  21388  irinitoringc  21396  pzriprnglem13  21410  pzriprnglem14  21411  zrhval2  21425  zrhpsgnmhm  21500  zfbas  23790  uzrest  23791  tgpmulg2  23988  zdis  24712  sszcld  24713  iscmet3lem3  25197  mbfsup  25572  tayl0  26276  ulmval  26296  ulmpm  26299  ulmf2  26300  dchrptlem2  27183  dchrptlem3  27184  elrgspnlem1  33200  elrgspnlem2  33201  elrgspnlem3  33202  elrgspnlem4  33203  elrgspn  33204  elrgspnsubrunlem1  33205  elrgspnsubrun  33207  qqhval  33969  dya2iocuni  34281  eulerpartgbij  34370  eulerpartlemmf  34373  ballotlemfval  34488  reprval  34608  divcnvlin  35727  heibor1lem  37810  aks6d1c6isolem2  42170  mzpclall  42722  mzpf  42731  mzpindd  42741  mzpsubst  42743  mzprename  42744  mzpcompact2lem  42746  diophrw  42754  lzenom  42765  diophin  42767  diophun  42768  eq0rabdioph  42771  eqrabdioph  42772  rabdiophlem1  42796  diophren  42808  hashnzfzclim  44318  uzct  45064  oddiadd  48166  2zrngadd  48235  2zrngmul  48243  zlmodzxzldeplem1  48493  digfval  48590