Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > zex | Structured version Visualization version GIF version |
Description: The set of integers exists. See also zexALT 12082. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 17-Nov-2014.) |
Ref | Expression |
---|---|
zex | ⊢ ℤ ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnex 10696 | . 2 ⊢ ℂ ∈ V | |
2 | zsscn 12070 | . 2 ⊢ ℤ ⊆ ℂ | |
3 | 1, 2 | ssexi 5190 | 1 ⊢ ℤ ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2114 Vcvv 3398 ℂcc 10613 ℤcz 12062 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-ext 2710 ax-sep 5167 ax-cnex 10671 ax-resscn 10672 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-ex 1787 df-sb 2075 df-clab 2717 df-cleq 2730 df-clel 2811 df-rab 3062 df-v 3400 df-un 3848 df-in 3850 df-ss 3860 df-sn 4517 df-pr 4519 df-op 4523 df-uni 4797 df-br 5031 df-iota 6297 df-fv 6347 df-ov 7173 df-neg 10951 df-z 12063 |
This theorem is referenced by: dfuzi 12154 uzval 12326 uzf 12327 fzval 12983 fzf 12985 climz 14996 climaddc1 15082 climmulc2 15084 climsubc1 15085 climsubc2 15086 climlec2 15108 iseraltlem1 15131 divcnvshft 15303 znnen 15657 lcmfval 16062 lcmf0val 16063 odzval 16228 mulgfval 18344 mulgfvalALT 18345 odinf 18808 odhash 18817 zaddablx 19111 zringplusg 20296 zringmulr 20298 zringmpg 20312 zrhval2 20329 zrhpsgnmhm 20400 zfbas 22647 uzrest 22648 tgpmulg2 22845 zdis 23568 sszcld 23569 iscmet3lem3 24042 mbfsup 24416 tayl0 25109 ulmval 25127 ulmpm 25130 ulmf2 25131 dchrptlem2 26001 dchrptlem3 26002 qqhval 31494 dya2iocuni 31820 eulerpartgbij 31909 eulerpartlemmf 31912 ballotlemfval 32026 reprval 32160 divcnvlin 33269 heibor1lem 35590 mzpclall 40121 mzpf 40130 mzpindd 40140 mzpsubst 40142 mzprename 40143 mzpcompact2lem 40145 diophrw 40153 lzenom 40164 diophin 40166 diophun 40167 eq0rabdioph 40170 eqrabdioph 40171 rabdiophlem1 40195 diophren 40207 hashnzfzclim 41478 uzct 42149 oddiadd 44902 2zrngadd 45029 2zrngmul 45037 irinitoringc 45161 zlmodzxzldeplem1 45375 digfval 45477 |
Copyright terms: Public domain | W3C validator |