![]() |
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 12575. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 17-Nov-2014.) |
Ref | Expression |
---|---|
zex | ⊢ ℤ ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnex 11187 | . 2 ⊢ ℂ ∈ V | |
2 | zsscn 12563 | . 2 ⊢ ℤ ⊆ ℂ | |
3 | 1, 2 | ssexi 5312 | 1 ⊢ ℤ ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2098 Vcvv 3466 ℂcc 11104 ℤcz 12555 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2695 ax-sep 5289 ax-cnex 11162 ax-resscn 11163 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2702 df-cleq 2716 df-clel 2802 df-rab 3425 df-v 3468 df-dif 3943 df-un 3945 df-in 3947 df-ss 3957 df-nul 4315 df-if 4521 df-sn 4621 df-pr 4623 df-op 4627 df-uni 4900 df-br 5139 df-iota 6485 df-fv 6541 df-ov 7404 df-neg 11444 df-z 12556 |
This theorem is referenced by: dfuzi 12650 uzval 12821 uzf 12822 fzval 13483 fzf 13485 climz 15490 climaddc1 15576 climmulc2 15578 climsubc1 15579 climsubc2 15580 climlec2 15602 iseraltlem1 15625 divcnvshft 15798 znnen 16152 lcmfval 16555 lcmf0val 16556 odzval 16723 mulgfval 18987 mulgfvalALT 18988 odinf 19473 odhash 19484 zaddablx 19782 zringplusg 21309 zringmulr 21312 zringmpg 21326 irinitoringc 21334 pzriprnglem13 21348 pzriprnglem14 21349 zrhval2 21363 zrhpsgnmhm 21445 zfbas 23722 uzrest 23723 tgpmulg2 23920 zdis 24654 sszcld 24655 iscmet3lem3 25140 mbfsup 25515 tayl0 26215 ulmval 26233 ulmpm 26236 ulmf2 26237 dchrptlem2 27114 dchrptlem3 27115 qqhval 33443 dya2iocuni 33771 eulerpartgbij 33860 eulerpartlemmf 33863 ballotlemfval 33977 reprval 34111 divcnvlin 35197 heibor1lem 37167 mzpclall 41954 mzpf 41963 mzpindd 41973 mzpsubst 41975 mzprename 41976 mzpcompact2lem 41978 diophrw 41986 lzenom 41997 diophin 41999 diophun 42000 eq0rabdioph 42003 eqrabdioph 42004 rabdiophlem1 42028 diophren 42040 hashnzfzclim 43570 uzct 44238 oddiadd 47037 2zrngadd 47106 2zrngmul 47114 zlmodzxzldeplem1 47369 digfval 47471 |
Copyright terms: Public domain | W3C validator |