Theorem zex 9487

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

Assertion

Ref	Expression
zex	⊢ ℤ ∈ V

Proof of Theorem zex

Step	Hyp	Ref	Expression
1		cnex 8155	. 2 ⊢ ℂ ∈ V
2		zsscn 9486	. 2 ⊢ ℤ ⊆ ℂ
3	1, 2	ssexi 4227	1 ⊢ ℤ ∈ V

Syntax hints:   ∈ wcel 2202  Vcvv 2802  ℂcc 8029  ℤcz 9478

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-sep 4207  ax-cnex 8122  ax-resscn 8123

This theorem depends on definitions:  df-bi 117  df-3or 1005  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516  df-rab 2519  df-v 2804  df-un 3204  df-in 3206  df-ss 3213  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-iota 5286  df-fv 5334  df-ov 6020  df-neg 8352  df-z 9479

This theorem is referenced by:  dfuzi  9589  uzval  9756  uzf  9757  fzval  10244  fzf  10246  flval  10531  frec2uzrand  10666  frec2uzf1od  10667  frecfzennn  10687  uzennn  10697  hashinfom  11039  climz  11852  serclim0  11865  climaddc1  11889  climmulc2  11891  climsubc1  11892  climsubc2  11893  climle  11894  climlec2  11901  iserabs  12035  isumshft  12050  explecnv  12065  prodfclim1  12104  qnumval  12756  qdenval  12757  odzval  12813  znnen  13018  exmidunben  13046  qnnen  13051  fngsum  13470  igsumvalx  13471  mulgfvalg  13707  mulgex  13709  zringplusg  14610  zringmulr  14612  zringmpg  14619  zrhval2  14632  lmres  14971  climcncf  15307