Theorem zex 9233

Description: The set of integers exists. (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 7910	. 2 |- CC e. _V
2		zsscn 9232	. 2 |- ZZ C_ CC
3	1, 2	ssexi 4136	1 |- ZZ e. _V

Syntax hints:   e. wcel 2146   _Vcvv 2735   CCcc 7784   ZZcz 9224

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157  ax-sep 4116  ax-cnex 7877  ax-resscn 7878

This theorem depends on definitions:  df-bi 117  df-3or 979  df-3an 980  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-rex 2459  df-rab 2462  df-v 2737  df-un 3131  df-in 3133  df-ss 3140  df-sn 3595  df-pr 3596  df-op 3598  df-uni 3806  df-br 3999  df-iota 5170  df-fv 5216  df-ov 5868  df-neg 8105  df-z 9225

This theorem is referenced by:  dfuzi  9334  uzval  9501  uzf  9502  fzval  9979  fzf  9981  flval  10240  frec2uzrand  10373  frec2uzf1od  10374  frecfzennn  10394  uzennn  10404  hashinfom  10724  climz  11266  serclim0  11279  climaddc1  11303  climmulc2  11305  climsubc1  11306  climsubc2  11307  climle  11308  climlec2  11315  iserabs  11449  isumshft  11464  explecnv  11479  prodfclim1  11518  qnumval  12150  qdenval  12151  odzval  12206  znnen  12364  exmidunben  12392  qnnen  12397  mulgfvalg  12844  lmres  13299  climcncf  13622