![]() |
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 12580. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 17-Nov-2014.) |
Ref | Expression |
---|---|
zex | ⊢ ℤ ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnex 11193 | . 2 ⊢ ℂ ∈ V | |
2 | zsscn 12568 | . 2 ⊢ ℤ ⊆ ℂ | |
3 | 1, 2 | ssexi 5322 | 1 ⊢ ℤ ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2106 Vcvv 3474 ℂcc 11110 ℤcz 12560 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2703 ax-sep 5299 ax-cnex 11168 ax-resscn 11169 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-rab 3433 df-v 3476 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-br 5149 df-iota 6495 df-fv 6551 df-ov 7414 df-neg 11449 df-z 12561 |
This theorem is referenced by: dfuzi 12655 uzval 12826 uzf 12827 fzval 13488 fzf 13490 climz 15495 climaddc1 15581 climmulc2 15583 climsubc1 15584 climsubc2 15585 climlec2 15607 iseraltlem1 15630 divcnvshft 15803 znnen 16157 lcmfval 16560 lcmf0val 16561 odzval 16726 mulgfval 18954 mulgfvalALT 18955 odinf 19433 odhash 19444 zaddablx 19742 zringplusg 21030 zringmulr 21033 zringmpg 21047 zrhval2 21064 zrhpsgnmhm 21143 zfbas 23407 uzrest 23408 tgpmulg2 23605 zdis 24339 sszcld 24340 iscmet3lem3 24814 mbfsup 25188 tayl0 25881 ulmval 25899 ulmpm 25902 ulmf2 25903 dchrptlem2 26775 dchrptlem3 26776 qqhval 33023 dya2iocuni 33351 eulerpartgbij 33440 eulerpartlemmf 33443 ballotlemfval 33557 reprval 33691 divcnvlin 34777 heibor1lem 36769 mzpclall 41553 mzpf 41562 mzpindd 41572 mzpsubst 41574 mzprename 41575 mzpcompact2lem 41577 diophrw 41585 lzenom 41596 diophin 41598 diophun 41599 eq0rabdioph 41602 eqrabdioph 41603 rabdiophlem1 41627 diophren 41639 hashnzfzclim 43169 uzct 43838 oddiadd 46669 pzriprnglem13 46902 pzriprnglem14 46903 2zrngadd 46920 2zrngmul 46928 irinitoringc 47052 zlmodzxzldeplem1 47265 digfval 47367 |
Copyright terms: Public domain | W3C validator |