![]() |
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 12578. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 17-Nov-2014.) |
Ref | Expression |
---|---|
zex | ⊢ ℤ ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnex 11191 | . 2 ⊢ ℂ ∈ V | |
2 | zsscn 12566 | . 2 ⊢ ℤ ⊆ ℂ | |
3 | 1, 2 | ssexi 5323 | 1 ⊢ ℤ ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2107 Vcvv 3475 ℂcc 11108 ℤcz 12558 |
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 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 ax-sep 5300 ax-cnex 11166 ax-resscn 11167 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-rab 3434 df-v 3477 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-br 5150 df-iota 6496 df-fv 6552 df-ov 7412 df-neg 11447 df-z 12559 |
This theorem is referenced by: dfuzi 12653 uzval 12824 uzf 12825 fzval 13486 fzf 13488 climz 15493 climaddc1 15579 climmulc2 15581 climsubc1 15582 climsubc2 15583 climlec2 15605 iseraltlem1 15628 divcnvshft 15801 znnen 16155 lcmfval 16558 lcmf0val 16559 odzval 16724 mulgfval 18952 mulgfvalALT 18953 odinf 19431 odhash 19442 zaddablx 19740 zringplusg 21024 zringmulr 21027 zringmpg 21041 zrhval2 21058 zrhpsgnmhm 21137 zfbas 23400 uzrest 23401 tgpmulg2 23598 zdis 24332 sszcld 24333 iscmet3lem3 24807 mbfsup 25181 tayl0 25874 ulmval 25892 ulmpm 25895 ulmf2 25896 dchrptlem2 26768 dchrptlem3 26769 qqhval 32954 dya2iocuni 33282 eulerpartgbij 33371 eulerpartlemmf 33374 ballotlemfval 33488 reprval 33622 divcnvlin 34702 heibor1lem 36677 mzpclall 41465 mzpf 41474 mzpindd 41484 mzpsubst 41486 mzprename 41487 mzpcompact2lem 41489 diophrw 41497 lzenom 41508 diophin 41510 diophun 41511 eq0rabdioph 41514 eqrabdioph 41515 rabdiophlem1 41539 diophren 41551 hashnzfzclim 43081 uzct 43750 oddiadd 46584 pzriprnglem13 46817 pzriprnglem14 46818 2zrngadd 46835 2zrngmul 46843 irinitoringc 46967 zlmodzxzldeplem1 47181 digfval 47283 |
Copyright terms: Public domain | W3C validator |