![]() |
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 11116. See also cnexALT 12920. (Contributed by Mario Carneiro, 17-Nov-2014.) |
Ref | Expression |
---|---|
cnex | ⊢ ℂ ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-cnex 11116 | 1 ⊢ ℂ ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2106 Vcvv 3446 ℂcc 11058 |
This theorem was proved from axioms: ax-cnex 11116 |
This theorem is referenced by: reex 11151 cnelprrecn 11153 pnfex 11217 nnex 12168 zex 12517 qex 12895 addex 12922 mulex 12923 rlim 15389 rlimf 15395 rlimss 15396 elo12 15421 o1f 15423 o1dm 15424 cnso 16140 cnaddablx 19660 cnaddabl 19661 cnaddid 19662 cnaddinv 19663 cnfldbas 20837 cnfldcj 20840 cnfldds 20843 cnfldfun 20845 cnfldfunALT 20846 cnfldfunALTOLD 20847 cnmsubglem 20897 cnmsgngrp 21020 psgninv 21023 lmbrf 22648 lmfss 22684 lmres 22688 lmcnp 22692 cnmet 24172 cncfval 24288 elcncf 24289 cncfcnvcn 24325 cnheibor 24355 cnlmodlem1 24536 tcphex 24618 tchnmfval 24629 tcphcph 24638 lmmbr2 24660 lmmbrf 24663 iscau2 24678 iscauf 24681 caucfil 24684 cmetcaulem 24689 caussi 24698 causs 24699 lmclimf 24705 mbff 25026 ismbf 25029 ismbfcn 25030 mbfconst 25034 mbfres 25045 mbfimaopn2 25058 cncombf 25059 cnmbf 25060 0plef 25073 0pledm 25074 itg1ge0 25087 mbfi1fseqlem5 25121 itg2addlem 25160 limcfval 25273 limcrcl 25275 ellimc2 25278 limcflf 25282 limcres 25287 limcun 25296 dvfval 25298 dvbss 25302 dvbsss 25303 perfdvf 25304 dvreslem 25310 dvres2lem 25311 dvcnp2 25321 dvnfval 25323 dvnff 25324 dvnf 25328 dvnbss 25329 dvnadd 25330 dvn2bss 25331 dvnres 25332 cpnfval 25333 cpnord 25336 dvaddbr 25339 dvmulbr 25340 dvnfre 25353 dvexp 25354 dvef 25381 c1liplem1 25397 c1lip2 25399 lhop1lem 25414 plyval 25591 elply 25593 elply2 25594 plyf 25596 plyss 25597 elplyr 25599 plyeq0lem 25608 plyeq0 25609 plypf1 25610 plyaddlem1 25611 plymullem1 25612 plyaddlem 25613 plymullem 25614 plysub 25617 coeeulem 25622 coeeq 25625 dgrlem 25627 coeidlem 25635 plyco 25639 coe0 25654 coesub 25655 dgrmulc 25669 dgrsub 25670 dgrcolem1 25671 dgrcolem2 25672 plymul0or 25678 dvnply2 25684 plycpn 25686 plydivlem3 25692 plydivlem4 25693 plydiveu 25695 plyremlem 25701 plyrem 25702 facth 25703 fta1lem 25704 quotcan 25706 vieta1lem2 25708 plyexmo 25710 elqaalem3 25718 qaa 25720 iaa 25722 aannenlem1 25725 aannenlem2 25726 aannenlem3 25727 taylfvallem1 25753 taylfval 25755 tayl0 25758 taylplem1 25759 taylply2 25764 taylply 25765 dvtaylp 25766 dvntaylp 25767 dvntaylp0 25768 taylthlem1 25769 taylthlem2 25770 ulmval 25776 ulmss 25793 ulmcn 25795 mtest 25800 pserulm 25818 psercn 25822 pserdvlem2 25824 abelth 25837 reefgim 25846 cxpcn2 26136 logbmpt 26175 logbfval 26177 lgamgulmlem5 26419 lgamgulmlem6 26420 lgamgulm2 26422 lgamcvglem 26426 ftalem7 26465 dchrfi 26640 cffldtocusgr 28458 isvcOLD 29584 cnaddabloOLD 29586 cnnvg 29683 cnnvs 29685 cnnvnm 29686 cncph 29824 hvmulex 30016 hfsmval 30743 hfmmval 30744 nmfnval 30881 nlfnval 30886 elcnfn 30887 ellnfn 30888 specval 30903 hhcnf 30910 lmlim 32617 esumcvg 32774 plymul02 33247 plymulx0 33248 signsplypnf 33251 signsply0 33252 breprexplemb 33333 breprexpnat 33336 vtsval 33339 circlemethnat 33343 circlevma 33344 circlemethhgt 33345 cvxpconn 33923 fwddifval 34823 fwddifnval 34824 ivthALT 34883 knoppcnlem5 35036 knoppcnlem8 35039 bj-inftyexpiinv 35752 bj-inftyexpidisj 35754 caures 36292 cntotbnd 36328 cnpwstotbnd 36329 rrnval 36359 cnaddcom 37507 elmnc 41521 mpaaeu 41535 itgoval 41546 itgocn 41549 rngunsnply 41558 binomcxplemnotnn0 42758 climexp 43966 xlimbr 44188 fuzxrpmcn 44189 xlimmnfvlem2 44194 xlimpnfvlem2 44198 mulcncff 44231 subcncff 44241 addcncff 44245 cncfuni 44247 divcncff 44252 dvsinax 44274 dvcosax 44287 dvnmptdivc 44299 dvnmptconst 44302 dvnxpaek 44303 dvnmul 44304 dvnprodlem3 44309 etransclem1 44596 etransclem2 44597 etransclem4 44599 etransclem13 44608 etransclem46 44641 fdivpm 46749 amgmlemALT 47370 |
Copyright terms: Public domain | W3C validator |