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

Theorem zex 10864
Description: The set of integers exists. See also zexALT 10874. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 17-Nov-2014.)
Assertion
Ref Expression
zex  |-  ZZ  e.  _V

Proof of Theorem zex
StepHypRef Expression
1 cnex 9564 . 2  |-  CC  e.  _V
2 zsscn 10863 . 2  |-  ZZ  C_  CC
31, 2ssexi 4587 1  |-  ZZ  e.  _V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1762   _Vcvv 3108   CCcc 9481   ZZcz 10855
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440  ax-sep 4563  ax-cnex 9539  ax-resscn 9540
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 969  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-rex 2815  df-rab 2818  df-v 3110  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3781  df-if 3935  df-sn 4023  df-pr 4025  df-op 4029  df-uni 4241  df-br 4443  df-iota 5544  df-fv 5589  df-ov 6280  df-neg 9799  df-z 10856
This theorem is referenced by:  dfuzi  10942  uzval  11075  uzf  11076  fzval  11665  fzf  11667  wrdexg  12512  climz  13323  climaddc1  13408  climmulc2  13410  climsubc1  13411  climsubc2  13412  climlec2  13432  iseraltlem1  13455  znnen  13798  odzval  14168  1arithlem1  14291  1arith  14295  mulgfval  15938  odinf  16376  odhash  16385  zaddablx  16662  zringplusg  18258  zringmulr  18260  zrngplusg  18264  zrngmulr  18266  dvdsrz  18270  zlpirlem3  18278  zringmpg  18284  prmirredlemOLD  18288  zrhval2  18308  zrhpsgnmhm  18382  zfbas  20127  uzrest  20128  tgpmulg2  20323  zdis  21051  sszcld  21052  iscmet3lem3  21459  mbfsup  21801  tayl0  22486  ulmval  22504  ulmpm  22507  ulmf2  22508  musum  23190  dchrptlem2  23263  dchrptlem3  23264  gxfval  24923  qqhval  27579  dya2iocuni  27882  eulerpartgbij  27939  eulerpartlemmf  27942  ballotlemfval  28056  divcnvshft  28582  divcnvlin  28583  heibor1lem  29897  mzpclall  30252  mzpf  30261  mzpindd  30271  mzpmfpOLD  30273  mzpsubst  30274  mzprename  30275  mzpcompact2lem  30277  diophrw  30285  lzenom  30296  diophin  30299  diophun  30300  eq0rabdioph  30303  eqrabdioph  30304  rabdiophlem1  30327  diophren  30340  zlmodzxzldeplem1  32059
  Copyright terms: Public domain W3C validator