Theorem zex 11386

Description: The set of integers exists. See also zexALT 11396. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 17-Nov-2014.)

Assertion

Ref	Expression
zex	|- ZZ e. _V

Proof of Theorem zex

Step	Hyp	Ref	Expression
1		cnex 10017	. 2 |- CC e. _V
2		zsscn 11385	. 2 |- ZZ C_ CC
3	1, 2	ssexi 4803	1 |- ZZ e. _V

Syntax hints:   e. wcel 1990   _Vcvv 3200   CCcc 9934   ZZcz 11377

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-cnex 9992  ax-resscn 9993

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653  df-neg 10269  df-z 11378

This theorem is referenced by:  dfuzi  11468  uzval  11689  uzf  11690  fzval  12328  fzf  12330  wrdexg  13315  climz  14280  climaddc1  14365  climmulc2  14367  climsubc1  14368  climsubc2  14369  climlec2  14389  iseraltlem1  14412  divcnvshft  14587  znnen  14941  lcmfval  15334  lcmf0val  15335  odzval  15496  1arithlem1  15627  1arith  15631  mulgfval  17542  odinf  17980  odhash  17989  zaddablx  18275  zringplusg  19825  zringmulr  19827  zringmpg  19840  zrhval2  19857  zrhpsgnmhm  19930  zfbas  21700  uzrest  21701  tgpmulg2  21898  zdis  22619  sszcld  22620  iscmet3lem3  23088  mbfsup  23431  tayl0  24116  ulmval  24134  ulmpm  24137  ulmf2  24138  musum  24917  dchrptlem2  24990  dchrptlem3  24991  qqhval  30018  dya2iocuni  30345  eulerpartgbij  30434  eulerpartlemmf  30437  ballotlemfval  30551  reprval  30688  divcnvlin  31618  heibor1lem  33608  mzpclall  37290  mzpf  37299  mzpindd  37309  mzpsubst  37311  mzprename  37312  mzpcompact2lem  37314  diophrw  37322  lzenom  37333  diophin  37336  diophun  37337  eq0rabdioph  37340  eqrabdioph  37341  rabdiophlem1  37365  diophren  37377  hashnzfzclim  38521  uzct  39232  oddiadd  41814  2zrngadd  41937  2zrngmul  41945  irinitoringc  42069  zlmodzxzldeplem1  42289  digfval  42391