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 11396. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 17-Nov-2014.) |
Ref | Expression |
---|---|
zex | ⊢ ℤ ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnex 10017 | . 2 ⊢ ℂ ∈ V | |
2 | zsscn 11385 | . 2 ⊢ ℤ ⊆ ℂ | |
3 | 1, 2 | ssexi 4803 | 1 ⊢ ℤ ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 1990 Vcvv 3200 ℂcc 9934 ℤcz 11377 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-cnex 9992 ax-resscn 9993 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-rex 2918 df-rab 2921 df-v 3202 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-sn 4178 df-pr 4180 df-op 4184 df-uni 4437 df-br 4654 df-iota 5851 df-fv 5896 df-ov 6653 df-neg 10269 df-z 11378 |
This theorem is referenced by: dfuzi 11468 uzval 11689 uzf 11690 fzval 12328 fzf 12330 wrdexg 13315 climz 14280 climaddc1 14365 climmulc2 14367 climsubc1 14368 climsubc2 14369 climlec2 14389 iseraltlem1 14412 divcnvshft 14587 znnen 14941 lcmfval 15334 lcmf0val 15335 odzval 15496 1arithlem1 15627 1arith 15631 mulgfval 17542 odinf 17980 odhash 17989 zaddablx 18275 zringplusg 19825 zringmulr 19827 zringmpg 19840 zrhval2 19857 zrhpsgnmhm 19930 zfbas 21700 uzrest 21701 tgpmulg2 21898 zdis 22619 sszcld 22620 iscmet3lem3 23088 mbfsup 23431 tayl0 24116 ulmval 24134 ulmpm 24137 ulmf2 24138 musum 24917 dchrptlem2 24990 dchrptlem3 24991 qqhval 30018 dya2iocuni 30345 eulerpartgbij 30434 eulerpartlemmf 30437 ballotlemfval 30551 reprval 30688 divcnvlin 31618 heibor1lem 33608 mzpclall 37290 mzpf 37299 mzpindd 37309 mzpsubst 37311 mzprename 37312 mzpcompact2lem 37314 diophrw 37322 lzenom 37333 diophin 37336 diophun 37337 eq0rabdioph 37340 eqrabdioph 37341 rabdiophlem1 37365 diophren 37377 hashnzfzclim 38521 uzct 39232 oddiadd 41814 2zrngadd 41937 2zrngmul 41945 irinitoringc 42069 zlmodzxzldeplem1 42289 digfval 42391 |
Copyright terms: Public domain | W3C validator |