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 10927. See also cnexALT 12726. (Contributed by Mario Carneiro, 17-Nov-2014.) |
Ref | Expression |
---|---|
cnex | ⊢ ℂ ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-cnex 10927 | 1 ⊢ ℂ ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2106 Vcvv 3432 ℂcc 10869 |
This theorem was proved from axioms: ax-cnex 10927 |
This theorem is referenced by: reex 10962 cnelprrecn 10964 pnfex 11028 nnex 11979 zex 12328 qex 12701 addex 12728 mulex 12729 rlim 15204 rlimf 15210 rlimss 15211 elo12 15236 o1f 15238 o1dm 15239 cnso 15956 cnaddablx 19469 cnaddabl 19470 cnaddid 19471 cnaddinv 19472 cnfldbas 20601 cnfldcj 20604 cnfldds 20607 cnfldfun 20609 cnfldfunALT 20610 cnfldfunALTOLD 20611 cnmsubglem 20661 cnmsgngrp 20784 psgninv 20787 lmbrf 22411 lmfss 22447 lmres 22451 lmcnp 22455 cnmet 23935 cncfval 24051 elcncf 24052 cncfcnvcn 24088 cnheibor 24118 cnlmodlem1 24299 tcphex 24381 tchnmfval 24392 tcphcph 24401 lmmbr2 24423 lmmbrf 24426 iscau2 24441 iscauf 24444 caucfil 24447 cmetcaulem 24452 caussi 24461 causs 24462 lmclimf 24468 mbff 24789 ismbf 24792 ismbfcn 24793 mbfconst 24797 mbfres 24808 mbfimaopn2 24821 cncombf 24822 cnmbf 24823 0plef 24836 0pledm 24837 itg1ge0 24850 mbfi1fseqlem5 24884 itg2addlem 24923 limcfval 25036 limcrcl 25038 ellimc2 25041 limcflf 25045 limcres 25050 limcun 25059 dvfval 25061 dvbss 25065 dvbsss 25066 perfdvf 25067 dvreslem 25073 dvres2lem 25074 dvcnp2 25084 dvnfval 25086 dvnff 25087 dvnf 25091 dvnbss 25092 dvnadd 25093 dvn2bss 25094 dvnres 25095 cpnfval 25096 cpnord 25099 dvaddbr 25102 dvmulbr 25103 dvnfre 25116 dvexp 25117 dvef 25144 c1liplem1 25160 c1lip2 25162 lhop1lem 25177 plyval 25354 elply 25356 elply2 25357 plyf 25359 plyss 25360 elplyr 25362 plyeq0lem 25371 plyeq0 25372 plypf1 25373 plyaddlem1 25374 plymullem1 25375 plyaddlem 25376 plymullem 25377 plysub 25380 coeeulem 25385 coeeq 25388 dgrlem 25390 coeidlem 25398 plyco 25402 coe0 25417 coesub 25418 dgrmulc 25432 dgrsub 25433 dgrcolem1 25434 dgrcolem2 25435 plymul0or 25441 dvnply2 25447 plycpn 25449 plydivlem3 25455 plydivlem4 25456 plydiveu 25458 plyremlem 25464 plyrem 25465 facth 25466 fta1lem 25467 quotcan 25469 vieta1lem2 25471 plyexmo 25473 elqaalem3 25481 qaa 25483 iaa 25485 aannenlem1 25488 aannenlem2 25489 aannenlem3 25490 taylfvallem1 25516 taylfval 25518 tayl0 25521 taylplem1 25522 taylply2 25527 taylply 25528 dvtaylp 25529 dvntaylp 25530 dvntaylp0 25531 taylthlem1 25532 taylthlem2 25533 ulmval 25539 ulmss 25556 ulmcn 25558 mtest 25563 pserulm 25581 psercn 25585 pserdvlem2 25587 abelth 25600 reefgim 25609 cxpcn2 25899 logbmpt 25938 logbfval 25940 lgamgulmlem5 26182 lgamgulmlem6 26183 lgamgulm2 26185 lgamcvglem 26189 ftalem7 26228 dchrfi 26403 cffldtocusgr 27814 isvcOLD 28941 cnaddabloOLD 28943 cnnvg 29040 cnnvs 29042 cnnvnm 29043 cncph 29181 hvmulex 29373 hfsmval 30100 hfmmval 30101 nmfnval 30238 nlfnval 30243 elcnfn 30244 ellnfn 30245 specval 30260 hhcnf 30267 lmlim 31897 esumcvg 32054 plymul02 32525 plymulx0 32526 signsplypnf 32529 signsply0 32530 breprexplemb 32611 breprexpnat 32614 vtsval 32617 circlemethnat 32621 circlevma 32622 circlemethhgt 32623 cvxpconn 33204 fwddifval 34464 fwddifnval 34465 ivthALT 34524 knoppcnlem5 34677 knoppcnlem8 34680 bj-inftyexpiinv 35379 bj-inftyexpidisj 35381 caures 35918 cntotbnd 35954 cnpwstotbnd 35955 rrnval 35985 cnaddcom 36986 elmnc 40961 mpaaeu 40975 itgoval 40986 itgocn 40989 rngunsnply 40998 binomcxplemnotnn0 41974 climexp 43146 xlimbr 43368 fuzxrpmcn 43369 xlimmnfvlem2 43374 xlimpnfvlem2 43378 mulcncff 43411 subcncff 43421 addcncff 43425 cncfuni 43427 divcncff 43432 dvsinax 43454 dvcosax 43467 dvnmptdivc 43479 dvnmptconst 43482 dvnxpaek 43483 dvnmul 43484 dvnprodlem3 43489 etransclem1 43776 etransclem2 43777 etransclem4 43779 etransclem13 43788 etransclem46 43821 fdivpm 45889 amgmlemALT 46507 |
Copyright terms: Public domain | W3C validator |