![]() |
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 11434. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 17-Nov-2014.) |
Ref | Expression |
---|---|
zex | ⊢ ℤ ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnex 10055 | . 2 ⊢ ℂ ∈ V | |
2 | zsscn 11423 | . 2 ⊢ ℤ ⊆ ℂ | |
3 | 1, 2 | ssexi 4836 | 1 ⊢ ℤ ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2030 Vcvv 3231 ℂcc 9972 ℤcz 11415 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 ax-sep 4814 ax-cnex 10030 ax-resscn 10031 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1055 df-3an 1056 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-rex 2947 df-rab 2950 df-v 3233 df-dif 3610 df-un 3612 df-in 3614 df-ss 3621 df-nul 3949 df-if 4120 df-sn 4211 df-pr 4213 df-op 4217 df-uni 4469 df-br 4686 df-iota 5889 df-fv 5934 df-ov 6693 df-neg 10307 df-z 11416 |
This theorem is referenced by: dfuzi 11506 uzval 11727 uzf 11728 fzval 12366 fzf 12368 wrdexg 13347 climz 14324 climaddc1 14409 climmulc2 14411 climsubc1 14412 climsubc2 14413 climlec2 14433 iseraltlem1 14456 divcnvshft 14631 znnen 14985 lcmfval 15381 lcmf0val 15382 odzval 15543 1arithlem1 15674 1arith 15678 mulgfval 17589 odinf 18026 odhash 18035 zaddablx 18321 zringplusg 19873 zringmulr 19875 zringmpg 19888 zrhval2 19905 zrhpsgnmhm 19978 zfbas 21747 uzrest 21748 tgpmulg2 21945 zdis 22666 sszcld 22667 iscmet3lem3 23134 mbfsup 23476 tayl0 24161 ulmval 24179 ulmpm 24182 ulmf2 24183 musum 24962 dchrptlem2 25035 dchrptlem3 25036 qqhval 30146 dya2iocuni 30473 eulerpartgbij 30562 eulerpartlemmf 30565 ballotlemfval 30679 reprval 30816 divcnvlin 31744 heibor1lem 33738 mzpclall 37607 mzpf 37616 mzpindd 37626 mzpsubst 37628 mzprename 37629 mzpcompact2lem 37631 diophrw 37639 lzenom 37650 diophin 37653 diophun 37654 eq0rabdioph 37657 eqrabdioph 37658 rabdiophlem1 37682 diophren 37694 hashnzfzclim 38838 uzct 39546 oddiadd 42139 2zrngadd 42262 2zrngmul 42270 irinitoringc 42394 zlmodzxzldeplem1 42614 digfval 42716 |
Copyright terms: Public domain | W3C validator |