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

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

Proof of Theorem zex
StepHypRef Expression
1 cnex 9594 . 2
2 zsscn 10897 . 2
31, 2ssexi 4597 1
Colors of variables: wff setvar class
Syntax hints:  e.wcel 1818   cvv 3109   cc 9511   cz 10889
This theorem is referenced by:  dfuzi  10978  uzval  11112  uzf  11113  fzval  11703  fzf  11705  wrdexg  12557  climz  13372  climaddc1  13457  climmulc2  13459  climsubc1  13460  climsubc2  13461  climlec2  13481  iseraltlem1  13504  znnen  13946  odzval  14318  1arithlem1  14441  1arith  14445  mulgfval  16143  odinf  16585  odhash  16594  zaddablx  16876  zringplusg  18495  zringmulr  18497  zrngplusg  18502  zrngmulr  18504  dvdsrz  18508  zlpirlem3  18516  zringmpg  18522  prmirredlemOLD  18526  zrhval2  18546  zrhpsgnmhm  18620  zfbas  20397  uzrest  20398  tgpmulg2  20593  zdis  21321  sszcld  21322  iscmet3lem3  21729  mbfsup  22071  tayl0  22757  ulmval  22775  ulmpm  22778  ulmf2  22779  musum  23467  dchrptlem2  23540  dchrptlem3  23541  gxfval  25259  qqhval  27955  dya2iocuni  28254  eulerpartgbij  28311  eulerpartlemmf  28314  ballotlemfval  28428  divcnvshft  29117  divcnvlin  29118  heibor1lem  30305  mzpclall  30659  mzpf  30668  mzpindd  30678  mzpmfpOLD  30680  mzpsubst  30681  mzprename  30682  mzpcompact2lem  30684  diophrw  30692  lzenom  30703  diophin  30706  diophun  30707  eq0rabdioph  30710  eqrabdioph  30711  rabdiophlem1  30734  diophren  30747  hashnzfzclim  31227  oddiadd  32502  2zrngadd  32743  2zrngmul  32751  irinitoringc  32877  zlmodzxzldeplem1  33101
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-cnex 9569  ax-resscn 9570
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-iota 5556  df-fv 5601  df-ov 6299  df-neg 9831  df-z 10890
  Copyright terms: Public domain W3C validator