![]() |
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 10582. See also cnexALT 12373. (Contributed by Mario Carneiro, 17-Nov-2014.) |
Ref | Expression |
---|---|
cnex | ⊢ ℂ ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-cnex 10582 | 1 ⊢ ℂ ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2111 Vcvv 3441 ℂcc 10524 |
This theorem was proved from axioms: ax-cnex 10582 |
This theorem is referenced by: reex 10617 cnelprrecn 10619 pnfex 10683 nnex 11631 zex 11978 qex 12348 addex 12375 mulex 12376 rlim 14844 rlimf 14850 rlimss 14851 elo12 14876 o1f 14878 o1dm 14879 cnso 15592 cnaddablx 18981 cnaddabl 18982 cnaddid 18983 cnaddinv 18984 cnfldbas 20095 cnfldcj 20098 cnfldds 20101 cnfldfun 20103 cnfldfunALT 20104 cnmsubglem 20154 cnmsgngrp 20268 psgninv 20271 lmbrf 21865 lmfss 21901 lmres 21905 lmcnp 21909 cnmet 23377 cncfval 23493 elcncf 23494 cncfcnvcn 23530 cnheibor 23560 cnlmodlem1 23741 tcphex 23821 tchnmfval 23832 tcphcph 23841 lmmbr2 23863 lmmbrf 23866 iscau2 23881 iscauf 23884 caucfil 23887 cmetcaulem 23892 caussi 23901 causs 23902 lmclimf 23908 mbff 24229 ismbf 24232 ismbfcn 24233 mbfconst 24237 mbfres 24248 mbfimaopn2 24261 cncombf 24262 cnmbf 24263 0plef 24276 0pledm 24277 itg1ge0 24290 mbfi1fseqlem5 24323 itg2addlem 24362 limcfval 24475 limcrcl 24477 ellimc2 24480 limcflf 24484 limcres 24489 limcun 24498 dvfval 24500 dvbss 24504 dvbsss 24505 perfdvf 24506 dvreslem 24512 dvres2lem 24513 dvcnp2 24523 dvnfval 24525 dvnff 24526 dvnf 24530 dvnbss 24531 dvnadd 24532 dvn2bss 24533 dvnres 24534 cpnfval 24535 cpnord 24538 dvaddbr 24541 dvmulbr 24542 dvnfre 24555 dvexp 24556 dvef 24583 c1liplem1 24599 c1lip2 24601 lhop1lem 24616 plyval 24790 elply 24792 elply2 24793 plyf 24795 plyss 24796 elplyr 24798 plyeq0lem 24807 plyeq0 24808 plypf1 24809 plyaddlem1 24810 plymullem1 24811 plyaddlem 24812 plymullem 24813 plysub 24816 coeeulem 24821 coeeq 24824 dgrlem 24826 coeidlem 24834 plyco 24838 coe0 24853 coesub 24854 dgrmulc 24868 dgrsub 24869 dgrcolem1 24870 dgrcolem2 24871 plymul0or 24877 dvnply2 24883 plycpn 24885 plydivlem3 24891 plydivlem4 24892 plydiveu 24894 plyremlem 24900 plyrem 24901 facth 24902 fta1lem 24903 quotcan 24905 vieta1lem2 24907 plyexmo 24909 elqaalem3 24917 qaa 24919 iaa 24921 aannenlem1 24924 aannenlem2 24925 aannenlem3 24926 taylfvallem1 24952 taylfval 24954 tayl0 24957 taylplem1 24958 taylply2 24963 taylply 24964 dvtaylp 24965 dvntaylp 24966 dvntaylp0 24967 taylthlem1 24968 taylthlem2 24969 ulmval 24975 ulmss 24992 ulmcn 24994 mtest 24999 pserulm 25017 psercn 25021 pserdvlem2 25023 abelth 25036 reefgim 25045 cxpcn2 25335 logbmpt 25374 logbfval 25376 lgamgulmlem5 25618 lgamgulmlem6 25619 lgamgulm2 25621 lgamcvglem 25625 ftalem7 25664 dchrfi 25839 cffldtocusgr 27237 isvcOLD 28362 cnaddabloOLD 28364 cnnvg 28461 cnnvs 28463 cnnvnm 28464 cncph 28602 hvmulex 28794 hfsmval 29521 hfmmval 29522 nmfnval 29659 nlfnval 29664 elcnfn 29665 ellnfn 29666 specval 29681 hhcnf 29688 lmlim 31300 esumcvg 31455 plymul02 31926 plymulx0 31927 signsplypnf 31930 signsply0 31931 breprexplemb 32012 breprexpnat 32015 vtsval 32018 circlemethnat 32022 circlevma 32023 circlemethhgt 32024 cvxpconn 32602 fwddifval 33736 fwddifnval 33737 ivthALT 33796 knoppcnlem5 33949 knoppcnlem8 33952 bj-inftyexpiinv 34623 bj-inftyexpidisj 34625 caures 35198 cntotbnd 35234 cnpwstotbnd 35235 rrnval 35265 cnaddcom 36268 elmnc 40080 mpaaeu 40094 itgoval 40105 itgocn 40108 rngunsnply 40117 binomcxplemnotnn0 41060 climexp 42247 xlimbr 42469 fuzxrpmcn 42470 xlimmnfvlem2 42475 xlimpnfvlem2 42479 mulcncff 42512 subcncff 42522 addcncff 42526 cncfuni 42528 divcncff 42533 dvsinax 42555 dvcosax 42568 dvnmptdivc 42580 dvnmptconst 42583 dvnxpaek 42584 dvnmul 42585 dvnprodlem3 42590 etransclem1 42877 etransclem2 42878 etransclem4 42880 etransclem13 42889 etransclem46 42922 fdivpm 44957 amgmlemALT 45331 |
Copyright terms: Public domain | W3C validator |