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 11032. See also cnexALT 12831. (Contributed by Mario Carneiro, 17-Nov-2014.) |
Ref | Expression |
---|---|
cnex | ⊢ ℂ ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-cnex 11032 | 1 ⊢ ℂ ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2106 Vcvv 3442 ℂcc 10974 |
This theorem was proved from axioms: ax-cnex 11032 |
This theorem is referenced by: reex 11067 cnelprrecn 11069 pnfex 11133 nnex 12084 zex 12433 qex 12806 addex 12833 mulex 12834 rlim 15303 rlimf 15309 rlimss 15310 elo12 15335 o1f 15337 o1dm 15338 cnso 16055 cnaddablx 19564 cnaddabl 19565 cnaddid 19566 cnaddinv 19567 cnfldbas 20706 cnfldcj 20709 cnfldds 20712 cnfldfun 20714 cnfldfunALT 20715 cnfldfunALTOLD 20716 cnmsubglem 20766 cnmsgngrp 20889 psgninv 20892 lmbrf 22516 lmfss 22552 lmres 22556 lmcnp 22560 cnmet 24040 cncfval 24156 elcncf 24157 cncfcnvcn 24193 cnheibor 24223 cnlmodlem1 24404 tcphex 24486 tchnmfval 24497 tcphcph 24506 lmmbr2 24528 lmmbrf 24531 iscau2 24546 iscauf 24549 caucfil 24552 cmetcaulem 24557 caussi 24566 causs 24567 lmclimf 24573 mbff 24894 ismbf 24897 ismbfcn 24898 mbfconst 24902 mbfres 24913 mbfimaopn2 24926 cncombf 24927 cnmbf 24928 0plef 24941 0pledm 24942 itg1ge0 24955 mbfi1fseqlem5 24989 itg2addlem 25028 limcfval 25141 limcrcl 25143 ellimc2 25146 limcflf 25150 limcres 25155 limcun 25164 dvfval 25166 dvbss 25170 dvbsss 25171 perfdvf 25172 dvreslem 25178 dvres2lem 25179 dvcnp2 25189 dvnfval 25191 dvnff 25192 dvnf 25196 dvnbss 25197 dvnadd 25198 dvn2bss 25199 dvnres 25200 cpnfval 25201 cpnord 25204 dvaddbr 25207 dvmulbr 25208 dvnfre 25221 dvexp 25222 dvef 25249 c1liplem1 25265 c1lip2 25267 lhop1lem 25282 plyval 25459 elply 25461 elply2 25462 plyf 25464 plyss 25465 elplyr 25467 plyeq0lem 25476 plyeq0 25477 plypf1 25478 plyaddlem1 25479 plymullem1 25480 plyaddlem 25481 plymullem 25482 plysub 25485 coeeulem 25490 coeeq 25493 dgrlem 25495 coeidlem 25503 plyco 25507 coe0 25522 coesub 25523 dgrmulc 25537 dgrsub 25538 dgrcolem1 25539 dgrcolem2 25540 plymul0or 25546 dvnply2 25552 plycpn 25554 plydivlem3 25560 plydivlem4 25561 plydiveu 25563 plyremlem 25569 plyrem 25570 facth 25571 fta1lem 25572 quotcan 25574 vieta1lem2 25576 plyexmo 25578 elqaalem3 25586 qaa 25588 iaa 25590 aannenlem1 25593 aannenlem2 25594 aannenlem3 25595 taylfvallem1 25621 taylfval 25623 tayl0 25626 taylplem1 25627 taylply2 25632 taylply 25633 dvtaylp 25634 dvntaylp 25635 dvntaylp0 25636 taylthlem1 25637 taylthlem2 25638 ulmval 25644 ulmss 25661 ulmcn 25663 mtest 25668 pserulm 25686 psercn 25690 pserdvlem2 25692 abelth 25705 reefgim 25714 cxpcn2 26004 logbmpt 26043 logbfval 26045 lgamgulmlem5 26287 lgamgulmlem6 26288 lgamgulm2 26290 lgamcvglem 26294 ftalem7 26333 dchrfi 26508 cffldtocusgr 28102 isvcOLD 29228 cnaddabloOLD 29230 cnnvg 29327 cnnvs 29329 cnnvnm 29330 cncph 29468 hvmulex 29660 hfsmval 30387 hfmmval 30388 nmfnval 30525 nlfnval 30530 elcnfn 30531 ellnfn 30532 specval 30547 hhcnf 30554 lmlim 32193 esumcvg 32350 plymul02 32823 plymulx0 32824 signsplypnf 32827 signsply0 32828 breprexplemb 32909 breprexpnat 32912 vtsval 32915 circlemethnat 32919 circlevma 32920 circlemethhgt 32921 cvxpconn 33501 fwddifval 34601 fwddifnval 34602 ivthALT 34661 knoppcnlem5 34814 knoppcnlem8 34817 bj-inftyexpiinv 35533 bj-inftyexpidisj 35535 caures 36074 cntotbnd 36110 cnpwstotbnd 36111 rrnval 36141 cnaddcom 37290 elmnc 41275 mpaaeu 41289 itgoval 41300 itgocn 41303 rngunsnply 41312 binomcxplemnotnn0 42347 climexp 43534 xlimbr 43756 fuzxrpmcn 43757 xlimmnfvlem2 43762 xlimpnfvlem2 43766 mulcncff 43799 subcncff 43809 addcncff 43813 cncfuni 43815 divcncff 43820 dvsinax 43842 dvcosax 43855 dvnmptdivc 43867 dvnmptconst 43870 dvnxpaek 43871 dvnmul 43872 dvnprodlem3 43877 etransclem1 44164 etransclem2 44165 etransclem4 44167 etransclem13 44176 etransclem46 44209 fdivpm 46307 amgmlemALT 46925 |
Copyright terms: Public domain | W3C validator |