Theorem zex 12480

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

Syntax hints:   ∈ wcel 2109  Vcvv 3436  ℂcc 11007  ℤcz 12471

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 2701  ax-sep 5235  ax-cnex 11065  ax-resscn 11066

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 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-iota 6438  df-fv 6490  df-ov 7352  df-neg 11350  df-z 12472

This theorem is referenced by:  dfuzi  12567  uzval  12737  uzf  12738  fzval  13412  fzf  13414  climz  15456  climaddc1  15542  climmulc2  15544  climsubc1  15545  climsubc2  15546  climlec2  15566  iseraltlem1  15589  divcnvshft  15762  znnen  16121  lcmfval  16532  lcmf0val  16533  odzval  16703  mulgfval  18948  mulgfvalALT  18949  odinf  19442  odhash  19453  zaddablx  19751  zringplusg  21361  zringmulr  21364  zringmpg  21378  irinitoringc  21386  pzriprnglem13  21400  pzriprnglem14  21401  zrhval2  21415  zrhpsgnmhm  21491  zfbas  23781  uzrest  23782  tgpmulg2  23979  zdis  24703  sszcld  24704  iscmet3lem3  25188  mbfsup  25563  tayl0  26267  ulmval  26287  ulmpm  26290  ulmf2  26291  dchrptlem2  27174  dchrptlem3  27175  elrgspnlem1  33182  elrgspnlem2  33183  elrgspnlem3  33184  elrgspnlem4  33185  elrgspn  33186  elrgspnsubrunlem1  33187  elrgspnsubrun  33189  qqhval  33939  dya2iocuni  34251  eulerpartgbij  34340  eulerpartlemmf  34343  ballotlemfval  34458  reprval  34578  divcnvlin  35706  heibor1lem  37789  aks6d1c6isolem2  42148  mzpclall  42700  mzpf  42709  mzpindd  42719  mzpsubst  42721  mzprename  42722  mzpcompact2lem  42724  diophrw  42732  lzenom  42743  diophin  42745  diophun  42746  eq0rabdioph  42749  eqrabdioph  42750  rabdiophlem1  42774  diophren  42786  hashnzfzclim  44295  uzct  45041  oddiadd  48158  2zrngadd  48227  2zrngmul  48235  zlmodzxzldeplem1  48485  digfval  48582