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

Theorem zex 10049
Description: The set of integers exists. See also zexALT 10058. (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 8834 . 2  |-  CC  e.  _V
2 zsscn 10048 . 2  |-  ZZ  C_  CC
31, 2ssexi 4175 1  |-  ZZ  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 1696   _Vcvv 2801   CCcc 8751   ZZcz 10040
This theorem is referenced by:  dfuzi  10118  uzval  10248  uzf  10249  fzval  10800  fzf  10802  wrdexg  11441  climz  12039  climaddc1  12124  climmulc2  12126  climsubc1  12127  climsubc2  12128  climlec2  12148  iseraltlem1  12170  znnen  12507  odzval  12872  1arithlem1  12986  1arith  12990  mulgfval  14584  odinf  14892  odhash  14901  zaddablx  15176  dvdsrz  16456  zlpirlem3  16459  prmirredlem  16462  zrhval2  16479  domnchr  16502  znunit  16533  znrrg  16535  cygznlem3  16539  zfbas  17607  uzrest  17608  tgpmulg2  17793  zdis  18338  iscmet3lem3  18732  mbfsup  19035  ulmval  19775  ulmpm  19778  ulmf2  19779  musum  20447  dchrzrhmul  20501  dchrptlem2  20520  dchrptlem3  20521  lgsdchr  20603  dchrisum0flblem1  20673  gxfval  20940  ballotlemfval  23064  dya2iocrfn  23595  dya2iocct  23596  dya2iocrrnval  23597  nZdef  25283  prodex  25407  lemindclsbu  26098  heibor1lem  26636  mzpclall  26908  mzpf  26917  mzpindd  26927  mzpmfp  26928  mzpsubst  26929  mzprename  26930  mzpcompact2lem  26932  diophrw  26941  lzenom  26952  diophin  26955  diophun  26956  eq0rabdioph  26959  eqrabdioph  26960  rabdiophlem1  26985  diophren  26999  climdivf  27841
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-cnex 8809  ax-resscn 8810
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rex 2562  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-iota 5235  df-fv 5279  df-ov 5877  df-neg 9056  df-z 10041
  Copyright terms: Public domain W3C validator