![]() |
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 10030. See also cnexALT 11866. (Contributed by Mario Carneiro, 17-Nov-2014.) |
Ref | Expression |
---|---|
cnex | ⊢ ℂ ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-cnex 10030 | 1 ⊢ ℂ ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2030 Vcvv 3231 ℂcc 9972 |
This theorem was proved from axioms: ax-cnex 10030 |
This theorem is referenced by: reex 10065 cnelprrecn 10067 pnfxr 10130 nnex 11064 zex 11424 qex 11838 addex 11868 mulex 11869 rlim 14270 rlimf 14276 rlimss 14277 elo12 14302 o1f 14304 o1dm 14305 cnso 15020 cnaddablx 18317 cnaddabl 18318 cnaddid 18319 cnaddinv 18320 cnfldbas 19798 cnfldcj 19801 cnfldds 19804 cnfldfun 19806 cnfldfunALT 19807 cnmsubglem 19857 cnmsgngrp 19973 psgninv 19976 lmbrf 21112 lmfss 21148 lmres 21152 lmcnp 21156 cnmet 22622 cncfval 22738 elcncf 22739 cncfcnvcn 22771 cnheibor 22801 cnlmodlem1 22982 tchex 23062 tchnmfval 23073 tchcph 23082 lmmbr2 23103 lmmbrf 23106 iscau2 23121 iscauf 23124 caucfil 23127 cmetcaulem 23132 caussi 23141 causs 23142 lmclimf 23148 mbff 23439 ismbf 23442 ismbfcn 23443 mbfconst 23447 mbfres 23456 mbfimaopn2 23469 cncombf 23470 cnmbf 23471 0plef 23484 0pledm 23485 itg1ge0 23498 mbfi1fseqlem5 23531 itg2addlem 23570 limcfval 23681 limcrcl 23683 ellimc2 23686 limcflf 23690 limcres 23695 limcun 23704 dvfval 23706 dvbss 23710 dvbsss 23711 perfdvf 23712 dvreslem 23718 dvres2lem 23719 dvcnp2 23728 dvnfval 23730 dvnff 23731 dvnf 23735 dvnbss 23736 dvnadd 23737 dvn2bss 23738 dvnres 23739 cpnfval 23740 cpnord 23743 dvaddbr 23746 dvmulbr 23747 dvnfre 23760 dvexp 23761 dvef 23788 c1liplem1 23804 c1lip2 23806 lhop1lem 23821 plyval 23994 elply 23996 elply2 23997 plyf 23999 plyss 24000 elplyr 24002 plyeq0lem 24011 plyeq0 24012 plypf1 24013 plyaddlem1 24014 plymullem1 24015 plyaddlem 24016 plymullem 24017 plysub 24020 coeeulem 24025 coeeq 24028 dgrlem 24030 coeidlem 24038 plyco 24042 coe0 24057 coesub 24058 dgrmulc 24072 dgrsub 24073 dgrcolem1 24074 dgrcolem2 24075 plymul0or 24081 dvnply2 24087 plycpn 24089 plydivlem3 24095 plydivlem4 24096 plydiveu 24098 plyremlem 24104 plyrem 24105 facth 24106 fta1lem 24107 quotcan 24109 vieta1lem2 24111 plyexmo 24113 elqaalem3 24121 qaa 24123 iaa 24125 aannenlem1 24128 aannenlem2 24129 aannenlem3 24130 taylfvallem1 24156 taylfval 24158 tayl0 24161 taylplem1 24162 taylply2 24167 taylply 24168 dvtaylp 24169 dvntaylp 24170 dvntaylp0 24171 taylthlem1 24172 taylthlem2 24173 ulmval 24179 ulmss 24196 ulmcn 24198 mtest 24203 pserulm 24221 psercn 24225 pserdvlem2 24227 abelth 24240 reefgim 24249 cxpcn2 24532 logbmpt 24571 logbfval 24573 lgamgulmlem5 24804 lgamgulmlem6 24805 lgamgulm2 24807 lgamcvglem 24811 ftalem7 24850 dchrfi 25025 cffldtocusgr 26399 isvcOLD 27562 cnaddabloOLD 27564 cnnvg 27661 cnnvs 27663 cnnvnm 27664 cncph 27802 hvmulex 27996 hfsmval 28725 hfmmval 28726 nmfnval 28863 nlfnval 28868 elcnfn 28869 ellnfn 28870 specval 28885 hhcnf 28892 lmlim 30121 esumcvg 30276 plymul02 30751 plymulx0 30752 signsplypnf 30755 signsply0 30756 breprexplemb 30837 breprexpnat 30840 vtsval 30843 circlemethnat 30847 circlevma 30848 circlemethhgt 30849 cvxpconn 31350 fwddifval 32394 fwddifnval 32395 ivthALT 32455 knoppcnlem5 32612 knoppcnlem8 32615 bj-inftyexpiinv 33225 bj-inftyexpidisj 33227 caures 33686 cntotbnd 33725 cnpwstotbnd 33726 rrnval 33756 cnaddcom 34577 elmnc 38023 mpaaeu 38037 itgoval 38048 itgocn 38051 rngunsnply 38060 binomcxplemnotnn0 38872 climexp 40155 xlimbr 40371 fuzxrpmcn 40372 xlimmnfvlem2 40377 xlimpnfvlem2 40381 mulcncff 40399 subcncff 40411 addcncff 40415 cncfuni 40417 divcncff 40422 dvsinax 40445 dvcosax 40459 dvnmptdivc 40471 dvnmptconst 40474 dvnxpaek 40475 dvnmul 40476 dvnprodlem3 40481 etransclem1 40770 etransclem2 40771 etransclem4 40773 etransclem13 40782 etransclem46 40815 fdivpm 42662 amgmlemALT 42877 |
Copyright terms: Public domain | W3C validator |