Theorem zex 9196

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 7873	. 2 |- CC e. _V
2		zsscn 9195	. 2 |- ZZ C_ CC
3	1, 2	ssexi 4119	1 |- ZZ e. _V

Syntax hints:   e. wcel 2136   _Vcvv 2725   CCcc 7747   ZZcz 9187

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147  ax-sep 4099  ax-cnex 7840  ax-resscn 7841

This theorem depends on definitions:  df-bi 116  df-3or 969  df-3an 970  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2296  df-rex 2449  df-rab 2452  df-v 2727  df-un 3119  df-in 3121  df-ss 3128  df-sn 3581  df-pr 3582  df-op 3584  df-uni 3789  df-br 3982  df-iota 5152  df-fv 5195  df-ov 5844  df-neg 8068  df-z 9188

This theorem is referenced by:  dfuzi  9297  uzval  9464  uzf  9465  fzval  9942  fzf  9944  flval  10203  frec2uzrand  10336  frec2uzf1od  10337  frecfzennn  10357  uzennn  10367  hashinfom  10687  climz  11229  serclim0  11242  climaddc1  11266  climmulc2  11268  climsubc1  11269  climsubc2  11270  climle  11271  climlec2  11278  iserabs  11412  isumshft  11427  explecnv  11442  prodfclim1  11481  qnumval  12113  qdenval  12114  odzval  12169  znnen  12327  exmidunben  12355  qnnen  12360  lmres  12848  climcncf  13171