| 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 11152. See also cnexALT 13006. (Contributed by Mario Carneiro, 17-Nov-2014.) |
| Ref | Expression |
|---|---|
| cnex | ⊢ ℂ ∈ V |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-cnex 11152 | 1 ⊢ ℂ ∈ V |
| Colors of variables: wff setvar class |
| Syntax hints: ∈ wcel 2149 Vcvv 3463 ℂcc 11094 |
| This theorem was proved from axioms: ax-cnex 11152 |
| This theorem is referenced by: reex 11187 cnelprrecn 11189 pnfex 11258 nnex 12235 zex 12596 qex 12981 mpoaddex 13008 addex 13009 mpomulex 13010 mulex 13011 rlim 15542 rlimf 15548 rlimss 15549 elo12 15574 o1f 15576 o1dm 15577 cnso 16299 cnaddablx 19934 cnaddabl 19935 cnaddid 19936 cnaddinv 19937 cnfldbas 21491 cnfldcj 21496 cnfldds 21499 cnfldfun 21501 cnfldfunALT 21502 cnmsubglem 21545 cnmsgngrp 21694 psgninv 21697 lmbrf 23382 lmfss 23418 lmres 23422 lmcnp 23426 cnmet 24893 cncfval 25012 elcncf 25013 cncfcnvcn 25049 cnheibor 25079 cnlmodlem1 25260 tcphex 25341 tchnmfval 25352 tcphcph 25361 lmmbr2 25383 lmmbrf 25386 iscau2 25401 iscauf 25404 caucfil 25407 cmetcaulem 25412 caussi 25421 causs 25422 lmclimf 25428 mbff 25749 ismbf 25752 ismbfcn 25753 mbfconst 25757 mbfres 25768 mbfimaopn2 25781 cncombf 25782 cnmbf 25783 0plef 25796 0pledm 25797 itg1ge0 25810 mbfi1fseqlem5 25843 itg2addlem 25882 limcfval 25996 limcrcl 25998 ellimc2 26001 limcflf 26005 limcres 26010 limcun 26019 dvfval 26021 dvbss 26025 dvbsss 26026 perfdvf 26027 dvreslem 26033 dvres2lem 26034 dvcnp2 26044 dvnfval 26046 dvnff 26047 dvnf 26051 dvnbss 26052 dvnadd 26053 dvn2bss 26054 dvnres 26055 cpnfval 26056 cpnord 26059 dvaddbr 26062 dvmulbr 26063 dvnfre 26076 dvexp 26077 dvef 26104 c1liplem1 26120 c1lip2 26122 lhop1lem 26137 plyval 26315 elply 26317 elply2 26318 plyf 26320 plyss 26321 elplyr 26323 plyeq0lem 26332 plyeq0 26333 plypf1 26334 plyaddlem1 26335 plymullem1 26336 plyaddlem 26337 plymullem 26338 plysub 26341 coeeulem 26346 coeeq 26349 dgrlem 26351 coeidlem 26359 plyco 26363 coe0 26378 coesub 26379 dgrmulc 26393 dgrsub 26394 dgrcolem1 26395 dgrcolem2 26396 plymul0or 26404 plymul02 26406 plyn0mulidp 26407 dvnply2 26413 plycpn 26415 plydivlem3 26421 plydivlem4 26422 plydiveu 26424 plyremlem 26430 plyrem 26431 facth 26432 fta1lem 26433 quotcan 26435 vieta1lem2 26437 plyexmo 26439 elqaalem3 26447 qaa 26449 iaa 26451 aannenlem1 26454 aannenlem2 26455 aannenlem3 26456 taylfvallem1 26482 taylfval 26484 tayl0 26487 taylplem1 26488 taylply2 26493 taylply 26494 dvtaylp 26495 dvntaylp 26496 dvntaylp0 26497 taylthlem1 26498 taylthlem2 26499 ulmval 26505 ulmss 26522 ulmcn 26524 mtest 26529 pserulm 26547 psercn 26551 pserdvlem2 26553 abelth 26566 reefgim 26575 cxpcn2 26873 logbmpt 26915 logbfval 26917 lgamgulmlem5 27159 lgamgulmlem6 27160 lgamgulm2 27162 lgamcvglem 27166 ftalem7 27205 dchrfi 27381 cffldtocusgr 29734 isvcOLD 30868 cnaddabloOLD 30870 cnnvg 30967 cnnvs 30969 cnnvnm 30970 cncph 31108 hvmulex 31300 hfsmval 32027 hfmmval 32028 nmfnval 32165 nlfnval 32170 elcnfn 32171 ellnfn 32172 specval 32187 hhcnf 32194 constrsuc 34069 lmlim 34278 esumcvg 34417 signsplypnf 34878 signsply0 34879 breprexplemb 34959 breprexpnat 34962 vtsval 34965 circlemethnat 34969 circlevma 34970 circlemethhgt 34971 cvxpconn 35629 fwddifval 36549 fwddifnval 36550 ivthALT 36731 knoppcnlem5 36971 knoppcnlem8 36974 bj-inftyexpiinv 37735 bj-inftyexpidisj 37737 caures 38294 cntotbnd 38330 cnpwstotbnd 38331 rrnval 38361 cnaddcom 39631 subex 42898 absex 42899 cjex 42900 elmnc 43748 mpaaeu 43762 itgoval 43773 itgocn 43776 rngunsnply 43781 binomcxplemnotnn0 44951 climexp 46206 xlimbr 46426 fuzxrpmcn 46427 xlimmnfvlem2 46432 xlimpnfvlem2 46436 mulcncff 46469 subcncff 46479 addcncff 46483 cncfuni 46485 divcncff 46490 dvsinax 46512 dvcosax 46525 dvnmptdivc 46537 dvnmptconst 46540 dvnxpaek 46541 dvnmul 46542 dvnprodlem3 46547 etransclem1 46834 etransclem2 46835 etransclem4 46837 etransclem13 46846 etransclem46 46879 nthrucw 47487 cjnpoly 47508 fdivpm 49201 amgmlemALT 50459 |
| Copyright terms: Public domain | W3C validator |