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

Theorem zex 10275
Description: The set of integers exists. See also zexALT 10284. (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 9055 . 2  |-  CC  e.  _V
2 zsscn 10274 . 2  |-  ZZ  C_  CC
31, 2ssexi 4335 1  |-  ZZ  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 1725   _Vcvv 2943   CCcc 8972   ZZcz 10266
This theorem is referenced by:  dfuzi  10344  uzval  10474  uzf  10475  fzval  11029  fzf  11031  wrdexg  11722  climz  12326  climaddc1  12411  climmulc2  12413  climsubc1  12414  climsubc2  12415  climlec2  12435  iseraltlem1  12458  znnen  12795  odzval  13160  1arithlem1  13274  1arith  13278  mulgfval  14874  odinf  15182  odhash  15191  zaddablx  15466  dvdsrz  16750  zlpirlem3  16753  prmirredlem  16756  zrhval2  16773  domnchr  16796  znunit  16827  znrrg  16829  cygznlem3  16833  zfbas  17911  uzrest  17912  tgpmulg2  18107  zdis  18830  sszcld  18831  iscmet3lem3  19226  mbfsup  19539  ulmval  20279  ulmpm  20282  ulmf2  20283  musum  20959  dchrzrhmul  21013  dchrptlem2  21032  dchrptlem3  21033  lgsdchr  21115  dchrisum0flblem1  21185  gxfval  21828  zzsplusg  24247  zzsmulr  24249  qqhval  24341  dya2iocuni  24616  ballotlemfval  24730  divcnvshft  25194  divcnvlin  25195  heibor1lem  26450  mzpclall  26716  mzpf  26725  mzpindd  26735  mzpmfp  26736  mzpsubst  26737  mzprename  26738  mzpcompact2lem  26740  diophrw  26749  lzenom  26760  diophin  26763  diophun  26764  eq0rabdioph  26767  eqrabdioph  26768  rabdiophlem1  26793  diophren  26806
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2411  ax-sep 4317  ax-cnex 9030  ax-resscn 9031
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2417  df-cleq 2423  df-clel 2426  df-nfc 2555  df-rex 2698  df-rab 2701  df-v 2945  df-dif 3310  df-un 3312  df-in 3314  df-ss 3321  df-nul 3616  df-if 3727  df-sn 3807  df-pr 3808  df-op 3810  df-uni 4003  df-br 4200  df-iota 5404  df-fv 5448  df-ov 6070  df-neg 9278  df-z 10267
  Copyright terms: Public domain W3C validator