![]() |
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 11747. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 17-Nov-2014.) |
Ref | Expression |
---|---|
zex | ⊢ ℤ ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnex 10353 | . 2 ⊢ ℂ ∈ V | |
2 | zsscn 11736 | . 2 ⊢ ℤ ⊆ ℂ | |
3 | 1, 2 | ssexi 5040 | 1 ⊢ ℤ ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2106 Vcvv 3397 ℂcc 10270 ℤcz 11728 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2054 ax-9 2115 ax-10 2134 ax-11 2149 ax-12 2162 ax-13 2333 ax-ext 2753 ax-sep 5017 ax-cnex 10328 ax-resscn 10329 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3or 1072 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2763 df-cleq 2769 df-clel 2773 df-nfc 2920 df-rex 3095 df-rab 3098 df-v 3399 df-dif 3794 df-un 3796 df-in 3798 df-ss 3805 df-nul 4141 df-if 4307 df-sn 4398 df-pr 4400 df-op 4404 df-uni 4672 df-br 4887 df-iota 6099 df-fv 6143 df-ov 6925 df-neg 10609 df-z 11729 |
This theorem is referenced by: dfuzi 11820 uzval 11994 uzf 11995 fzval 12645 fzf 12647 wrdexgOLD 13610 climz 14688 climaddc1 14773 climmulc2 14775 climsubc1 14776 climsubc2 14777 climlec2 14797 iseraltlem1 14820 divcnvshft 14991 znnen 15345 lcmfval 15740 lcmf0val 15741 odzval 15900 mulgfval 17929 odinf 18364 odhash 18373 zaddablx 18661 zringplusg 20221 zringmulr 20223 zringmpg 20236 zrhval2 20253 zrhpsgnmhm 20325 zfbas 22108 uzrest 22109 tgpmulg2 22306 zdis 23027 sszcld 23028 iscmet3lem3 23496 mbfsup 23868 tayl0 24553 ulmval 24571 ulmpm 24574 ulmf2 24575 musum 25369 dchrptlem2 25442 dchrptlem3 25443 qqhval 30616 dya2iocuni 30943 eulerpartgbij 31032 eulerpartlemmf 31035 ballotlemfval 31150 reprval 31290 divcnvlin 32212 heibor1lem 34227 mzpclall 38243 mzpf 38252 mzpindd 38262 mzpsubst 38264 mzprename 38265 mzpcompact2lem 38267 diophrw 38275 lzenom 38286 diophin 38289 diophun 38290 eq0rabdioph 38293 eqrabdioph 38294 rabdiophlem1 38318 diophren 38330 hashnzfzclim 39470 uzct 40156 oddiadd 42822 2zrngadd 42945 2zrngmul 42953 irinitoringc 43077 zlmodzxzldeplem1 43297 digfval 43399 |
Copyright terms: Public domain | W3C validator |