Theorem zex 12538

Description: The set of integers exists. See also zexALT 12549. (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 11149	. 2 ⊢ ℂ ∈ V
2		zsscn 12537	. 2 ⊢ ℤ ⊆ ℂ
3	1, 2	ssexi 5277	1 ⊢ ℤ ∈ V

Syntax hints:   ∈ wcel 2109  Vcvv 3447  ℂcc 11066  ℤcz 12529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-cnex 11124  ax-resscn 11125

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390  df-neg 11408  df-z 12530

This theorem is referenced by:  dfuzi  12625  uzval  12795  uzf  12796  fzval  13470  fzf  13472  climz  15515  climaddc1  15601  climmulc2  15603  climsubc1  15604  climsubc2  15605  climlec2  15625  iseraltlem1  15648  divcnvshft  15821  znnen  16180  lcmfval  16591  lcmf0val  16592  odzval  16762  mulgfval  19001  mulgfvalALT  19002  odinf  19493  odhash  19504  zaddablx  19802  zringplusg  21364  zringmulr  21367  zringmpg  21381  irinitoringc  21389  pzriprnglem13  21403  pzriprnglem14  21404  zrhval2  21418  zrhpsgnmhm  21493  zfbas  23783  uzrest  23784  tgpmulg2  23981  zdis  24705  sszcld  24706  iscmet3lem3  25190  mbfsup  25565  tayl0  26269  ulmval  26289  ulmpm  26292  ulmf2  26293  dchrptlem2  27176  dchrptlem3  27177  elrgspnlem1  33193  elrgspnlem2  33194  elrgspnlem3  33195  elrgspnlem4  33196  elrgspn  33197  elrgspnsubrunlem1  33198  elrgspnsubrun  33200  qqhval  33962  dya2iocuni  34274  eulerpartgbij  34363  eulerpartlemmf  34366  ballotlemfval  34481  reprval  34601  divcnvlin  35720  heibor1lem  37803  aks6d1c6isolem2  42163  mzpclall  42715  mzpf  42724  mzpindd  42734  mzpsubst  42736  mzprename  42737  mzpcompact2lem  42739  diophrw  42747  lzenom  42758  diophin  42760  diophun  42761  eq0rabdioph  42764  eqrabdioph  42765  rabdiophlem1  42789  diophren  42801  hashnzfzclim  44311  uzct  45057  oddiadd  48162  2zrngadd  48231  2zrngmul  48239  zlmodzxzldeplem1  48489  digfval  48586