Theorem zex 8729

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 7445	. 2 |- CC e. _V
2		zsscn 8728	. 2 |- ZZ C_ CC
3	1, 2	ssexi 3969	1 |- ZZ e. _V

Syntax hints:   e. wcel 1438   _Vcvv 2619   CCcc 7327   ZZcz 8720

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070  ax-sep 3949  ax-cnex 7415  ax-resscn 7416

This theorem depends on definitions:  df-bi 115  df-3or 925  df-3an 926  df-tru 1292  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-rex 2365  df-rab 2368  df-v 2621  df-un 3001  df-in 3003  df-ss 3010  df-sn 3447  df-pr 3448  df-op 3450  df-uni 3649  df-br 3838  df-iota 4967  df-fv 5010  df-ov 5637  df-neg 7635  df-z 8721

This theorem is referenced by:  dfuzi  8826  uzval  8990  uzf  8991  fzval  9395  fzf  9397  flval  9644  frec2uzrand  9777  frec2uzf1od  9778  frecfzennn  9798  hashinfom  10151  climz  10644  serclim0  10657  iserclim0  10658  climaddc1  10681  climmulc2  10683  climsubc1  10684  climsubc2  10685  climle  10686  climlec2  10694  isumshft  10846  explecnv  10860  qnumval  11256  qdenval  11257  znnen  11304