![]() |
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 10328. See also cnexALT 12133. (Contributed by Mario Carneiro, 17-Nov-2014.) |
Ref | Expression |
---|---|
cnex | ⊢ ℂ ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-cnex 10328 | 1 ⊢ ℂ ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2107 Vcvv 3398 ℂcc 10270 |
This theorem was proved from axioms: ax-cnex 10328 |
This theorem is referenced by: reex 10363 cnelprrecn 10365 pnfex 10429 nnex 11381 zex 11737 qex 12108 addex 12135 mulex 12136 rlim 14634 rlimf 14640 rlimss 14641 elo12 14666 o1f 14668 o1dm 14669 cnso 15380 cnaddablx 18657 cnaddabl 18658 cnaddid 18659 cnaddinv 18660 cnfldbas 20146 cnfldcj 20149 cnfldds 20152 cnfldfun 20154 cnfldfunALT 20155 cnmsubglem 20205 cnmsgngrp 20320 psgninv 20323 lmbrf 21472 lmfss 21508 lmres 21512 lmcnp 21516 cnmet 22983 cncfval 23099 elcncf 23100 cncfcnvcn 23132 cnheibor 23162 cnlmodlem1 23343 tcphex 23423 tchnmfval 23434 tcphcph 23443 lmmbr2 23465 lmmbrf 23468 iscau2 23483 iscauf 23486 caucfil 23489 cmetcaulem 23494 caussi 23503 causs 23504 lmclimf 23510 mbff 23829 ismbf 23832 ismbfcn 23833 mbfconst 23837 mbfres 23848 mbfimaopn2 23861 cncombf 23862 cnmbf 23863 0plef 23876 0pledm 23877 itg1ge0 23890 mbfi1fseqlem5 23923 itg2addlem 23962 limcfval 24073 limcrcl 24075 ellimc2 24078 limcflf 24082 limcres 24087 limcun 24096 dvfval 24098 dvbss 24102 dvbsss 24103 perfdvf 24104 dvreslem 24110 dvres2lem 24111 dvcnp2 24120 dvnfval 24122 dvnff 24123 dvnf 24127 dvnbss 24128 dvnadd 24129 dvn2bss 24130 dvnres 24131 cpnfval 24132 cpnord 24135 dvaddbr 24138 dvmulbr 24139 dvnfre 24152 dvexp 24153 dvef 24180 c1liplem1 24196 c1lip2 24198 lhop1lem 24213 plyval 24386 elply 24388 elply2 24389 plyf 24391 plyss 24392 elplyr 24394 plyeq0lem 24403 plyeq0 24404 plypf1 24405 plyaddlem1 24406 plymullem1 24407 plyaddlem 24408 plymullem 24409 plysub 24412 coeeulem 24417 coeeq 24420 dgrlem 24422 coeidlem 24430 plyco 24434 coe0 24449 coesub 24450 dgrmulc 24464 dgrsub 24465 dgrcolem1 24466 dgrcolem2 24467 plymul0or 24473 dvnply2 24479 plycpn 24481 plydivlem3 24487 plydivlem4 24488 plydiveu 24490 plyremlem 24496 plyrem 24497 facth 24498 fta1lem 24499 quotcan 24501 vieta1lem2 24503 plyexmo 24505 elqaalem3 24513 qaa 24515 iaa 24517 aannenlem1 24520 aannenlem2 24521 aannenlem3 24522 taylfvallem1 24548 taylfval 24550 tayl0 24553 taylplem1 24554 taylply2 24559 taylply 24560 dvtaylp 24561 dvntaylp 24562 dvntaylp0 24563 taylthlem1 24564 taylthlem2 24565 ulmval 24571 ulmss 24588 ulmcn 24590 mtest 24595 pserulm 24613 psercn 24617 pserdvlem2 24619 abelth 24632 reefgim 24641 cxpcn2 24927 logbmpt 24966 logbfval 24968 lgamgulmlem5 25211 lgamgulmlem6 25212 lgamgulm2 25214 lgamcvglem 25218 ftalem7 25257 dchrfi 25432 cffldtocusgr 26795 isvcOLD 28006 cnaddabloOLD 28008 cnnvg 28105 cnnvs 28107 cnnvnm 28108 cncph 28246 hvmulex 28440 hfsmval 29169 hfmmval 29170 nmfnval 29307 nlfnval 29312 elcnfn 29313 ellnfn 29314 specval 29329 hhcnf 29336 lmlim 30591 esumcvg 30746 plymul02 31223 plymulx0 31224 signsplypnf 31227 signsply0 31228 breprexplemb 31311 breprexpnat 31314 vtsval 31317 circlemethnat 31321 circlevma 31322 circlemethhgt 31323 cvxpconn 31823 fwddifval 32858 fwddifnval 32859 ivthALT 32918 knoppcnlem5 33070 knoppcnlem8 33073 bj-inftyexpiinv 33685 bj-inftyexpidisj 33687 caures 34180 cntotbnd 34219 cnpwstotbnd 34220 rrnval 34250 cnaddcom 35126 elmnc 38665 mpaaeu 38679 itgoval 38690 itgocn 38693 rngunsnply 38702 binomcxplemnotnn0 39511 climexp 40745 xlimbr 40967 fuzxrpmcn 40968 xlimmnfvlem2 40973 xlimpnfvlem2 40977 mulcncff 41009 subcncff 41021 addcncff 41025 cncfuni 41027 divcncff 41032 dvsinax 41055 dvcosax 41069 dvnmptdivc 41081 dvnmptconst 41084 dvnxpaek 41085 dvnmul 41086 dvnprodlem3 41091 etransclem1 41379 etransclem2 41380 etransclem4 41382 etransclem13 41391 etransclem46 41424 fdivpm 43352 amgmlemALT 43655 |
Copyright terms: Public domain | W3C validator |