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

Theorem zex 10642
Description: The set of integers exists. See also zexALT 10652. (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 9350 . 2  |-  CC  e.  _V
2 zsscn 10641 . 2  |-  ZZ  C_  CC
31, 2ssexi 4425 1  |-  ZZ  e.  _V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1755   _Vcvv 2962   CCcc 9267   ZZcz 10633
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-cnex 9325  ax-resscn 9326
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 959  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rex 2711  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-iota 5369  df-fv 5414  df-ov 6083  df-neg 9585  df-z 10634
This theorem is referenced by:  dfuzi  10719  uzval  10850  uzf  10851  fzval  11425  fzf  11427  wrdexg  12227  climz  13010  climaddc1  13095  climmulc2  13097  climsubc1  13098  climsubc2  13099  climlec2  13119  iseraltlem1  13142  znnen  13477  odzval  13845  1arithlem1  13966  1arith  13970  mulgfval  15607  odinf  16043  odhash  16052  zaddablx  16329  zringplusg  17731  zringmulr  17733  zrngplusg  17737  zrngmulr  17739  dvdsrz  17743  zlpirlem3  17751  zringmpg  17757  prmirredlemOLD  17761  zrhval2  17781  zrhpsgnmhm  17855  zfbas  19310  uzrest  19311  tgpmulg2  19506  zdis  20234  sszcld  20235  iscmet3lem3  20642  mbfsup  20983  tayl0  21711  ulmval  21729  ulmpm  21732  ulmf2  21733  musum  22415  dchrptlem2  22488  dchrptlem3  22489  gxfval  23566  qqhval  26256  dya2iocuni  26551  eulerpartgbij  26602  ballotlemfval  26719  divcnvshft  27244  divcnvlin  27245  heibor1lem  28549  mzpclall  28905  mzpf  28914  mzpindd  28924  mzpmfpOLD  28926  mzpsubst  28927  mzprename  28928  mzpcompact2lem  28930  diophrw  28939  lzenom  28950  diophin  28953  diophun  28954  eq0rabdioph  28957  eqrabdioph  28958  rabdiophlem1  28981  diophren  28994  zlmodzxzldeplem1  30748
  Copyright terms: Public domain W3C validator