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

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

Proof of Theorem zex
StepHypRef Expression
1 cnex 10201 . 2 ℂ ∈ V
2 zsscn 11569 . 2 ℤ ⊆ ℂ
31, 2ssexi 4947 1 ℤ ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2131  Vcvv 3332  cc 10118  cz 11561
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732  ax-sep 4925  ax-cnex 10176  ax-resscn 10177
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-rex 3048  df-rab 3051  df-v 3334  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-nul 4051  df-if 4223  df-sn 4314  df-pr 4316  df-op 4320  df-uni 4581  df-br 4797  df-iota 6004  df-fv 6049  df-ov 6808  df-neg 10453  df-z 11562
This theorem is referenced by:  dfuzi  11652  uzval  11873  uzf  11874  fzval  12513  fzf  12515  wrdexg  13493  climz  14471  climaddc1  14556  climmulc2  14558  climsubc1  14559  climsubc2  14560  climlec2  14580  iseraltlem1  14603  divcnvshft  14778  znnen  15132  lcmfval  15528  lcmf0val  15529  odzval  15690  1arithlem1  15821  1arith  15825  mulgfval  17735  odinf  18172  odhash  18181  zaddablx  18467  zringplusg  20019  zringmulr  20021  zringmpg  20034  zrhval2  20051  zrhpsgnmhm  20124  zfbas  21893  uzrest  21894  tgpmulg2  22091  zdis  22812  sszcld  22813  iscmet3lem3  23280  mbfsup  23622  tayl0  24307  ulmval  24325  ulmpm  24328  ulmf2  24329  musum  25108  dchrptlem2  25181  dchrptlem3  25182  qqhval  30319  dya2iocuni  30646  eulerpartgbij  30735  eulerpartlemmf  30738  ballotlemfval  30852  reprval  30989  divcnvlin  31917  heibor1lem  33913  mzpclall  37784  mzpf  37793  mzpindd  37803  mzpsubst  37805  mzprename  37806  mzpcompact2lem  37808  diophrw  37816  lzenom  37827  diophin  37830  diophun  37831  eq0rabdioph  37834  eqrabdioph  37835  rabdiophlem1  37859  diophren  37871  hashnzfzclim  39015  uzct  39723  oddiadd  42316  2zrngadd  42439  2zrngmul  42447  irinitoringc  42571  zlmodzxzldeplem1  42791  digfval  42893
  Copyright terms: Public domain W3C validator