| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > cnex | Structured version Visualization version GIF version | ||
| Description: Alias for ax-cnex 11085. See also cnexALT 12927. (Contributed by Mario Carneiro, 17-Nov-2014.) |
| Ref | Expression |
|---|---|
| cnex | ⊢ ℂ ∈ V |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-cnex 11085 | 1 ⊢ ℂ ∈ V |
| Colors of variables: wff setvar class |
| Syntax hints: ∈ wcel 2119 Vcvv 3431 ℂcc 11027 |
| This theorem was proved from axioms: ax-cnex 11085 |
| This theorem is referenced by: reex 11120 cnelprrecn 11122 pnfex 11189 nnex 12171 zex 12524 qex 12902 mpoaddex 12929 addex 12930 mpomulex 12931 mulex 12932 rlim 15448 rlimf 15454 rlimss 15455 elo12 15480 o1f 15482 o1dm 15483 cnso 16205 cnaddablx 19834 cnaddabl 19835 cnaddid 19836 cnaddinv 19837 cnfldbas 21351 cnfldcj 21356 cnfldds 21359 cnfldfun 21361 cnfldfunALT 21362 cnmsubglem 21405 cnmsgngrp 21554 psgninv 21557 lmbrf 23243 lmfss 23279 lmres 23283 lmcnp 23287 cnmet 24754 cncfval 24873 elcncf 24874 cncfcnvcn 24910 cnheibor 24940 cnlmodlem1 25121 tcphex 25202 tchnmfval 25213 tcphcph 25222 lmmbr2 25244 lmmbrf 25247 iscau2 25262 iscauf 25265 caucfil 25268 cmetcaulem 25273 caussi 25282 causs 25283 lmclimf 25289 mbff 25610 ismbf 25613 ismbfcn 25614 mbfconst 25618 mbfres 25629 mbfimaopn2 25642 cncombf 25643 cnmbf 25644 0plef 25657 0pledm 25658 itg1ge0 25671 mbfi1fseqlem5 25704 itg2addlem 25743 limcfval 25857 limcrcl 25859 ellimc2 25862 limcflf 25866 limcres 25871 limcun 25880 dvfval 25882 dvbss 25886 dvbsss 25887 perfdvf 25888 dvreslem 25894 dvres2lem 25895 dvcnp2 25905 dvnfval 25907 dvnff 25908 dvnf 25912 dvnbss 25913 dvnadd 25914 dvn2bss 25915 dvnres 25916 cpnfval 25917 cpnord 25920 dvaddbr 25923 dvmulbr 25924 dvnfre 25937 dvexp 25938 dvef 25965 c1liplem1 25981 c1lip2 25983 lhop1lem 25998 plyval 26176 elply 26178 elply2 26179 plyf 26181 plyss 26182 elplyr 26184 plyeq0lem 26193 plyeq0 26194 plypf1 26195 plyaddlem1 26196 plymullem1 26197 plyaddlem 26198 plymullem 26199 plysub 26202 coeeulem 26207 coeeq 26210 dgrlem 26212 coeidlem 26220 plyco 26224 coe0 26239 coesub 26240 dgrmulc 26254 dgrsub 26255 dgrcolem1 26256 dgrcolem2 26257 plymul0or 26265 dvnply2 26271 plycpn 26273 plydivlem3 26279 plydivlem4 26280 plydiveu 26282 plyremlem 26288 plyrem 26289 facth 26290 fta1lem 26291 quotcan 26293 vieta1lem2 26295 plyexmo 26297 elqaalem3 26305 qaa 26307 iaa 26309 aannenlem1 26312 aannenlem2 26313 aannenlem3 26314 taylfvallem1 26340 taylfval 26342 tayl0 26345 taylplem1 26346 taylply2 26351 taylply 26352 dvtaylp 26353 dvntaylp 26354 dvntaylp0 26355 taylthlem1 26356 taylthlem2 26357 ulmval 26363 ulmss 26380 ulmcn 26382 mtest 26387 pserulm 26405 psercn 26409 pserdvlem2 26411 abelth 26424 reefgim 26433 cxpcn2 26728 logbmpt 26770 logbfval 26772 lgamgulmlem5 27014 lgamgulmlem6 27015 lgamgulm2 27017 lgamcvglem 27021 ftalem7 27060 dchrfi 27236 cffldtocusgr 29534 isvcOLD 30668 cnaddabloOLD 30670 cnnvg 30767 cnnvs 30769 cnnvnm 30770 cncph 30908 hvmulex 31100 hfsmval 31827 hfmmval 31828 nmfnval 31965 nlfnval 31970 elcnfn 31971 ellnfn 31972 specval 31987 hhcnf 31994 constrsuc 33922 lmlim 34131 esumcvg 34270 plymul02 34730 plymulx0 34731 signsplypnf 34734 signsply0 34735 breprexplemb 34815 breprexpnat 34818 vtsval 34821 circlemethnat 34825 circlevma 34826 circlemethhgt 34827 cvxpconn 35470 fwddifval 36390 fwddifnval 36391 ivthALT 36563 knoppcnlem5 36803 knoppcnlem8 36806 bj-inftyexpiinv 37568 bj-inftyexpidisj 37570 caures 38127 cntotbnd 38163 cnpwstotbnd 38164 rrnval 38194 cnaddcom 39464 subex 42731 absex 42732 cjex 42733 elmnc 43581 mpaaeu 43595 itgoval 43606 itgocn 43609 rngunsnply 43614 binomcxplemnotnn0 44800 climexp 46050 xlimbr 46270 fuzxrpmcn 46271 xlimmnfvlem2 46276 xlimpnfvlem2 46280 mulcncff 46313 subcncff 46323 addcncff 46327 cncfuni 46329 divcncff 46334 dvsinax 46356 dvcosax 46369 dvnmptdivc 46381 dvnmptconst 46384 dvnxpaek 46385 dvnmul 46386 dvnprodlem3 46391 etransclem1 46678 etransclem2 46679 etransclem4 46681 etransclem13 46690 etransclem46 46723 nthrucw 47331 cjnpoly 47352 fdivpm 49034 amgmlemALT 50293 |
| Copyright terms: Public domain | W3C validator |