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 9871. See also cnexALT 11704. (Contributed by Mario Carneiro, 17-Nov-2014.) |
Ref | Expression |
---|---|
cnex | ⊢ ℂ ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-cnex 9871 | 1 ⊢ ℂ ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 1977 Vcvv 3173 ℂcc 9813 |
This theorem was proved from axioms: ax-cnex 9871 |
This theorem is referenced by: reex 9906 cnelprrecn 9908 pnfxr 9971 nnex 10903 zex 11263 qex 11676 addex 11706 mulex 11707 rlim 14074 rlimf 14080 rlimss 14081 elo12 14106 o1f 14108 o1dm 14109 cnso 14815 cnaddablx 18094 cnaddabl 18095 cnaddid 18096 cnaddinv 18097 cnfldbas 19571 cnfldcj 19574 cnfldds 19577 cnmsubglem 19628 cnmsgngrp 19744 psgninv 19747 lmbrf 20874 lmfss 20910 lmres 20914 lmcnp 20918 cnmet 22385 cncfval 22499 elcncf 22500 cncfcnvcn 22532 cnheibor 22562 cnlmodlem1 22744 tchex 22824 tchnmfval 22835 tchcph 22844 lmmbr2 22865 lmmbrf 22868 iscau2 22883 iscauf 22886 caucfil 22889 cmetcaulem 22894 caussi 22903 causs 22904 lmclimf 22910 mbff 23200 ismbf 23203 ismbfcn 23204 mbfconst 23208 mbfres 23217 mbfimaopn2 23230 cncombf 23231 cnmbf 23232 0plef 23245 0pledm 23246 itg1ge0 23259 mbfi1fseqlem5 23292 itg2addlem 23331 limcfval 23442 limcrcl 23444 ellimc2 23447 limcflf 23451 limcres 23456 limcun 23465 dvfval 23467 dvbss 23471 dvbsss 23472 perfdvf 23473 dvreslem 23479 dvres2lem 23480 dvcnp2 23489 dvnfval 23491 dvnff 23492 dvnf 23496 dvnbss 23497 dvnadd 23498 dvn2bss 23499 dvnres 23500 cpnfval 23501 cpnord 23504 dvaddbr 23507 dvmulbr 23508 dvnfre 23521 dvexp 23522 dvef 23547 c1liplem1 23563 c1lip2 23565 lhop1lem 23580 plyval 23753 elply 23755 elply2 23756 plyf 23758 plyss 23759 elplyr 23761 plyeq0lem 23770 plyeq0 23771 plypf1 23772 plyaddlem1 23773 plymullem1 23774 plyaddlem 23775 plymullem 23776 plysub 23779 coeeulem 23784 coeeq 23787 dgrlem 23789 coeidlem 23797 plyco 23801 coe0 23816 coesub 23817 dgrmulc 23831 dgrsub 23832 dgrcolem1 23833 dgrcolem2 23834 plymul0or 23840 dvnply2 23846 plycpn 23848 plydivlem3 23854 plydivlem4 23855 plydiveu 23857 plyremlem 23863 plyrem 23864 facth 23865 fta1lem 23866 quotcan 23868 vieta1lem2 23870 plyexmo 23872 elqaalem3 23880 qaa 23882 iaa 23884 aannenlem1 23887 aannenlem2 23888 aannenlem3 23889 taylfvallem1 23915 taylfval 23917 tayl0 23920 taylplem1 23921 taylply2 23926 taylply 23927 dvtaylp 23928 dvntaylp 23929 dvntaylp0 23930 taylthlem1 23931 taylthlem2 23932 ulmval 23938 ulmss 23955 ulmcn 23957 mtest 23962 pserulm 23980 psercn 23984 pserdvlem2 23986 abelth 23999 reefgim 24008 cxpcn2 24287 logbmpt 24326 logbfval 24328 lgamgulmlem5 24559 lgamgulmlem6 24560 lgamgulm2 24562 lgamcvglem 24566 ftalem7 24605 dchrfi 24780 isvcOLD 26818 cnaddabloOLD 26820 cnnvg 26917 cnnvs 26919 cnnvnm 26920 cncph 27058 hvmulex 27252 hfsmval 27981 hfmmval 27982 nmfnval 28119 nlfnval 28124 elcnfn 28125 ellnfn 28126 specval 28141 hhcnf 28148 lmlim 29321 esumcvg 29475 plymul02 29949 plymulx0 29950 signsplypnf 29953 signsply0 29954 cvxpcon 30478 fwddifval 31439 fwddifnval 31440 ivthALT 31500 knoppcnlem5 31657 knoppcnlem8 31660 bj-inftyexpiinv 32272 bj-inftyexpidisj 32274 caures 32726 cntotbnd 32765 cnpwstotbnd 32766 rrnval 32796 cnaddcom 33277 elmnc 36725 mpaaeu 36739 itgoval 36750 itgocn 36753 rngunsnply 36762 binomcxplemnotnn0 37577 climexp 38672 mulcncff 38753 subcncff 38765 addcncff 38770 cncfuni 38772 divcncff 38777 dvsinax 38801 dvcosax 38816 dvnmptdivc 38828 dvnmptconst 38831 dvnxpaek 38832 dvnmul 38833 dvnprodlem3 38838 etransclem1 39128 etransclem2 39129 etransclem4 39131 etransclem13 39140 etransclem46 39173 fdivpm 42135 amgmlemALT 42358 |
Copyright terms: Public domain | W3C validator |