| 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 11094. See also cnexALT 12936. (Contributed by Mario Carneiro, 17-Nov-2014.) |
| Ref | Expression |
|---|---|
| cnex | ⊢ ℂ ∈ V |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-cnex 11094 | 1 ⊢ ℂ ∈ V |
| Colors of variables: wff setvar class |
| Syntax hints: ∈ wcel 2114 Vcvv 3429 ℂcc 11036 |
| This theorem was proved from axioms: ax-cnex 11094 |
| This theorem is referenced by: reex 11129 cnelprrecn 11131 pnfex 11198 nnex 12180 zex 12533 qex 12911 mpoaddex 12938 addex 12939 mpomulex 12940 mulex 12941 rlim 15457 rlimf 15463 rlimss 15464 elo12 15489 o1f 15491 o1dm 15492 cnso 16214 cnaddablx 19843 cnaddabl 19844 cnaddid 19845 cnaddinv 19846 cnfldbas 21356 cnfldcj 21361 cnfldds 21364 cnfldfun 21366 cnfldfunALT 21367 cnmsubglem 21410 cnmsgngrp 21559 psgninv 21562 lmbrf 23225 lmfss 23261 lmres 23265 lmcnp 23269 cnmet 24736 cncfval 24855 elcncf 24856 cncfcnvcn 24892 cnheibor 24922 cnlmodlem1 25103 tcphex 25184 tchnmfval 25195 tcphcph 25204 lmmbr2 25226 lmmbrf 25229 iscau2 25244 iscauf 25247 caucfil 25250 cmetcaulem 25255 caussi 25264 causs 25265 lmclimf 25271 mbff 25592 ismbf 25595 ismbfcn 25596 mbfconst 25600 mbfres 25611 mbfimaopn2 25624 cncombf 25625 cnmbf 25626 0plef 25639 0pledm 25640 itg1ge0 25653 mbfi1fseqlem5 25686 itg2addlem 25725 limcfval 25839 limcrcl 25841 ellimc2 25844 limcflf 25848 limcres 25853 limcun 25862 dvfval 25864 dvbss 25868 dvbsss 25869 perfdvf 25870 dvreslem 25876 dvres2lem 25877 dvcnp2 25887 dvnfval 25889 dvnff 25890 dvnf 25894 dvnbss 25895 dvnadd 25896 dvn2bss 25897 dvnres 25898 cpnfval 25899 cpnord 25902 dvaddbr 25905 dvmulbr 25906 dvnfre 25919 dvexp 25920 dvef 25947 c1liplem1 25963 c1lip2 25965 lhop1lem 25980 plyval 26158 elply 26160 elply2 26161 plyf 26163 plyss 26164 elplyr 26166 plyeq0lem 26175 plyeq0 26176 plypf1 26177 plyaddlem1 26178 plymullem1 26179 plyaddlem 26180 plymullem 26181 plysub 26184 coeeulem 26189 coeeq 26192 dgrlem 26194 coeidlem 26202 plyco 26206 coe0 26221 coesub 26222 dgrmulc 26236 dgrsub 26237 dgrcolem1 26238 dgrcolem2 26239 plymul0or 26247 dvnply2 26253 plycpn 26255 plydivlem3 26261 plydivlem4 26262 plydiveu 26264 plyremlem 26270 plyrem 26271 facth 26272 fta1lem 26273 quotcan 26275 vieta1lem2 26277 plyexmo 26279 elqaalem3 26287 qaa 26289 iaa 26291 aannenlem1 26294 aannenlem2 26295 aannenlem3 26296 taylfvallem1 26322 taylfval 26324 tayl0 26327 taylplem1 26328 taylply2 26333 taylply 26334 dvtaylp 26335 dvntaylp 26336 dvntaylp0 26337 taylthlem1 26338 taylthlem2 26339 ulmval 26345 ulmss 26362 ulmcn 26364 mtest 26369 pserulm 26387 psercn 26391 pserdvlem2 26393 abelth 26406 reefgim 26415 cxpcn2 26710 logbmpt 26752 logbfval 26754 lgamgulmlem5 26996 lgamgulmlem6 26997 lgamgulm2 26999 lgamcvglem 27003 ftalem7 27042 dchrfi 27218 cffldtocusgr 29516 isvcOLD 30650 cnaddabloOLD 30652 cnnvg 30749 cnnvs 30751 cnnvnm 30752 cncph 30890 hvmulex 31082 hfsmval 31809 hfmmval 31810 nmfnval 31947 nlfnval 31952 elcnfn 31953 ellnfn 31954 specval 31969 hhcnf 31976 constrsuc 33882 lmlim 34091 esumcvg 34230 plymul02 34690 plymulx0 34691 signsplypnf 34694 signsply0 34695 breprexplemb 34775 breprexpnat 34778 vtsval 34781 circlemethnat 34785 circlevma 34786 circlemethhgt 34787 cvxpconn 35424 fwddifval 36344 fwddifnval 36345 ivthALT 36517 knoppcnlem5 36757 knoppcnlem8 36760 bj-inftyexpiinv 37522 bj-inftyexpidisj 37524 caures 38081 cntotbnd 38117 cnpwstotbnd 38118 rrnval 38148 cnaddcom 39418 subex 42686 absex 42687 cjex 42688 elmnc 43564 mpaaeu 43578 itgoval 43589 itgocn 43592 rngunsnply 43597 binomcxplemnotnn0 44783 climexp 46035 xlimbr 46255 fuzxrpmcn 46256 xlimmnfvlem2 46261 xlimpnfvlem2 46265 mulcncff 46298 subcncff 46308 addcncff 46312 cncfuni 46314 divcncff 46319 dvsinax 46341 dvcosax 46354 dvnmptdivc 46366 dvnmptconst 46369 dvnxpaek 46370 dvnmul 46371 dvnprodlem3 46376 etransclem1 46663 etransclem2 46664 etransclem4 46666 etransclem13 46675 etransclem46 46708 nthrucw 47316 cjnpoly 47337 fdivpm 49019 amgmlemALT 50278 |
| Copyright terms: Public domain | W3C validator |