![]() |
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 11166. See also cnexALT 12970. (Contributed by Mario Carneiro, 17-Nov-2014.) |
Ref | Expression |
---|---|
cnex | ⊢ ℂ ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-cnex 11166 | 1 ⊢ ℂ ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2107 Vcvv 3475 ℂcc 11108 |
This theorem was proved from axioms: ax-cnex 11166 |
This theorem is referenced by: reex 11201 cnelprrecn 11203 pnfex 11267 nnex 12218 zex 12567 qex 12945 addex 12972 mulex 12973 rlim 15439 rlimf 15445 rlimss 15446 elo12 15471 o1f 15473 o1dm 15474 cnso 16190 cnaddablx 19736 cnaddabl 19737 cnaddid 19738 cnaddinv 19739 cnfldbas 20948 cnfldcj 20951 cnfldds 20954 cnfldfun 20956 cnfldfunALT 20957 cnfldfunALTOLD 20958 cnmsubglem 21008 cnmsgngrp 21132 psgninv 21135 lmbrf 22764 lmfss 22800 lmres 22804 lmcnp 22808 cnmet 24288 cncfval 24404 elcncf 24405 cncfcnvcn 24441 cnheibor 24471 cnlmodlem1 24652 tcphex 24734 tchnmfval 24745 tcphcph 24754 lmmbr2 24776 lmmbrf 24779 iscau2 24794 iscauf 24797 caucfil 24800 cmetcaulem 24805 caussi 24814 causs 24815 lmclimf 24821 mbff 25142 ismbf 25145 ismbfcn 25146 mbfconst 25150 mbfres 25161 mbfimaopn2 25174 cncombf 25175 cnmbf 25176 0plef 25189 0pledm 25190 itg1ge0 25203 mbfi1fseqlem5 25237 itg2addlem 25276 limcfval 25389 limcrcl 25391 ellimc2 25394 limcflf 25398 limcres 25403 limcun 25412 dvfval 25414 dvbss 25418 dvbsss 25419 perfdvf 25420 dvreslem 25426 dvres2lem 25427 dvcnp2 25437 dvnfval 25439 dvnff 25440 dvnf 25444 dvnbss 25445 dvnadd 25446 dvn2bss 25447 dvnres 25448 cpnfval 25449 cpnord 25452 dvaddbr 25455 dvmulbr 25456 dvnfre 25469 dvexp 25470 dvef 25497 c1liplem1 25513 c1lip2 25515 lhop1lem 25530 plyval 25707 elply 25709 elply2 25710 plyf 25712 plyss 25713 elplyr 25715 plyeq0lem 25724 plyeq0 25725 plypf1 25726 plyaddlem1 25727 plymullem1 25728 plyaddlem 25729 plymullem 25730 plysub 25733 coeeulem 25738 coeeq 25741 dgrlem 25743 coeidlem 25751 plyco 25755 coe0 25770 coesub 25771 dgrmulc 25785 dgrsub 25786 dgrcolem1 25787 dgrcolem2 25788 plymul0or 25794 dvnply2 25800 plycpn 25802 plydivlem3 25808 plydivlem4 25809 plydiveu 25811 plyremlem 25817 plyrem 25818 facth 25819 fta1lem 25820 quotcan 25822 vieta1lem2 25824 plyexmo 25826 elqaalem3 25834 qaa 25836 iaa 25838 aannenlem1 25841 aannenlem2 25842 aannenlem3 25843 taylfvallem1 25869 taylfval 25871 tayl0 25874 taylplem1 25875 taylply2 25880 taylply 25881 dvtaylp 25882 dvntaylp 25883 dvntaylp0 25884 taylthlem1 25885 taylthlem2 25886 ulmval 25892 ulmss 25909 ulmcn 25911 mtest 25916 pserulm 25934 psercn 25938 pserdvlem2 25940 abelth 25953 reefgim 25962 cxpcn2 26254 logbmpt 26293 logbfval 26295 lgamgulmlem5 26537 lgamgulmlem6 26538 lgamgulm2 26540 lgamcvglem 26544 ftalem7 26583 dchrfi 26758 cffldtocusgr 28704 isvcOLD 29832 cnaddabloOLD 29834 cnnvg 29931 cnnvs 29933 cnnvnm 29934 cncph 30072 hvmulex 30264 hfsmval 30991 hfmmval 30992 nmfnval 31129 nlfnval 31134 elcnfn 31135 ellnfn 31136 specval 31151 hhcnf 31158 lmlim 32927 esumcvg 33084 plymul02 33557 plymulx0 33558 signsplypnf 33561 signsply0 33562 breprexplemb 33643 breprexpnat 33646 vtsval 33649 circlemethnat 33653 circlevma 33654 circlemethhgt 33655 cvxpconn 34233 fwddifval 35134 fwddifnval 35135 mpomulex 35161 gg-dvcnp2 35174 gg-dvmulbr 35175 ivthALT 35220 knoppcnlem5 35373 knoppcnlem8 35376 bj-inftyexpiinv 36089 bj-inftyexpidisj 36091 caures 36628 cntotbnd 36664 cnpwstotbnd 36665 rrnval 36695 cnaddcom 37842 elmnc 41878 mpaaeu 41892 itgoval 41903 itgocn 41906 rngunsnply 41915 binomcxplemnotnn0 43115 climexp 44321 xlimbr 44543 fuzxrpmcn 44544 xlimmnfvlem2 44549 xlimpnfvlem2 44553 mulcncff 44586 subcncff 44596 addcncff 44600 cncfuni 44602 divcncff 44607 dvsinax 44629 dvcosax 44642 dvnmptdivc 44654 dvnmptconst 44657 dvnxpaek 44658 dvnmul 44659 dvnprodlem3 44664 etransclem1 44951 etransclem2 44952 etransclem4 44954 etransclem13 44963 etransclem46 44996 fdivpm 47229 amgmlemALT 47850 |
Copyright terms: Public domain | W3C validator |