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 12339. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 17-Nov-2014.) |
Ref | Expression |
---|---|
zex | ⊢ ℤ ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnex 10952 | . 2 ⊢ ℂ ∈ V | |
2 | zsscn 12327 | . 2 ⊢ ℤ ⊆ ℂ | |
3 | 1, 2 | ssexi 5246 | 1 ⊢ ℤ ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2106 Vcvv 3432 ℂcc 10869 ℤcz 12319 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 ax-sep 5223 ax-cnex 10927 ax-resscn 10928 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-rab 3073 df-v 3434 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-nul 4257 df-if 4460 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-br 5075 df-iota 6391 df-fv 6441 df-ov 7278 df-neg 11208 df-z 12320 |
This theorem is referenced by: dfuzi 12411 uzval 12584 uzf 12585 fzval 13241 fzf 13243 climz 15258 climaddc1 15344 climmulc2 15346 climsubc1 15347 climsubc2 15348 climlec2 15370 iseraltlem1 15393 divcnvshft 15567 znnen 15921 lcmfval 16326 lcmf0val 16327 odzval 16492 mulgfval 18702 mulgfvalALT 18703 odinf 19170 odhash 19179 zaddablx 19473 zringplusg 20677 zringmulr 20679 zringmpg 20693 zrhval2 20710 zrhpsgnmhm 20789 zfbas 23047 uzrest 23048 tgpmulg2 23245 zdis 23979 sszcld 23980 iscmet3lem3 24454 mbfsup 24828 tayl0 25521 ulmval 25539 ulmpm 25542 ulmf2 25543 dchrptlem2 26413 dchrptlem3 26414 qqhval 31924 dya2iocuni 32250 eulerpartgbij 32339 eulerpartlemmf 32342 ballotlemfval 32456 reprval 32590 divcnvlin 33698 heibor1lem 35967 mzpclall 40549 mzpf 40558 mzpindd 40568 mzpsubst 40570 mzprename 40571 mzpcompact2lem 40573 diophrw 40581 lzenom 40592 diophin 40594 diophun 40595 eq0rabdioph 40598 eqrabdioph 40599 rabdiophlem1 40623 diophren 40635 hashnzfzclim 41940 uzct 42611 oddiadd 45368 2zrngadd 45495 2zrngmul 45503 irinitoringc 45627 zlmodzxzldeplem1 45841 digfval 45943 |
Copyright terms: Public domain | W3C validator |