MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  zex Structured version   Visualization version   GIF version

Theorem zex 11993
Description: The set of integers exists. See also zexALT 12004. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 17-Nov-2014.)
Assertion
Ref Expression
zex ℤ ∈ V

Proof of Theorem zex
StepHypRef Expression
1 cnex 10621 . 2 ℂ ∈ V
2 zsscn 11992 . 2 ℤ ⊆ ℂ
31, 2ssexi 5229 1 ℤ ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2113  Vcvv 3497  cc 10538  cz 11984
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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-sep 5206  ax-cnex 10596  ax-resscn 10597
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-rab 3150  df-v 3499  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4471  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4842  df-br 5070  df-iota 6317  df-fv 6366  df-ov 7162  df-neg 10876  df-z 11985
This theorem is referenced by:  dfuzi  12076  uzval  12248  uzf  12249  fzval  12897  fzf  12899  wrdexgOLD  13875  climz  14909  climaddc1  14994  climmulc2  14996  climsubc1  14997  climsubc2  14998  climlec2  15018  iseraltlem1  15041  divcnvshft  15213  znnen  15568  lcmfval  15968  lcmf0val  15969  odzval  16131  mulgfval  18229  mulgfvalALT  18230  odinf  18693  odhash  18702  zaddablx  18995  zringplusg  20627  zringmulr  20629  zringmpg  20642  zrhval2  20659  zrhpsgnmhm  20731  zfbas  22507  uzrest  22508  tgpmulg2  22705  zdis  23427  sszcld  23428  iscmet3lem3  23896  mbfsup  24268  tayl0  24953  ulmval  24971  ulmpm  24974  ulmf2  24975  dchrptlem2  25844  dchrptlem3  25845  qqhval  31219  dya2iocuni  31545  eulerpartgbij  31634  eulerpartlemmf  31637  ballotlemfval  31751  reprval  31885  divcnvlin  32968  heibor1lem  35091  mzpclall  39330  mzpf  39339  mzpindd  39349  mzpsubst  39351  mzprename  39352  mzpcompact2lem  39354  diophrw  39362  lzenom  39373  diophin  39375  diophun  39376  eq0rabdioph  39379  eqrabdioph  39380  rabdiophlem1  39404  diophren  39416  hashnzfzclim  40660  uzct  41331  oddiadd  44088  2zrngadd  44215  2zrngmul  44223  irinitoringc  44347  zlmodzxzldeplem1  44562  digfval  44664
  Copyright terms: Public domain W3C validator