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 10582. See also cnexALT 12375. (Contributed by Mario Carneiro, 17-Nov-2014.) |
Ref | Expression |
---|---|
cnex | ⊢ ℂ ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-cnex 10582 | 1 ⊢ ℂ ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2105 Vcvv 3495 ℂcc 10524 |
This theorem was proved from axioms: ax-cnex 10582 |
This theorem is referenced by: reex 10617 cnelprrecn 10619 pnfex 10683 nnex 11633 zex 11979 qex 12350 addex 12377 mulex 12378 rlim 14842 rlimf 14848 rlimss 14849 elo12 14874 o1f 14876 o1dm 14877 cnso 15590 cnaddablx 18919 cnaddabl 18920 cnaddid 18921 cnaddinv 18922 cnfldbas 20479 cnfldcj 20482 cnfldds 20485 cnfldfun 20487 cnfldfunALT 20488 cnmsubglem 20538 cnmsgngrp 20653 psgninv 20656 lmbrf 21798 lmfss 21834 lmres 21838 lmcnp 21842 cnmet 23309 cncfval 23425 elcncf 23426 cncfcnvcn 23458 cnheibor 23488 cnlmodlem1 23669 tcphex 23749 tchnmfval 23760 tcphcph 23769 lmmbr2 23791 lmmbrf 23794 iscau2 23809 iscauf 23812 caucfil 23815 cmetcaulem 23820 caussi 23829 causs 23830 lmclimf 23836 mbff 24155 ismbf 24158 ismbfcn 24159 mbfconst 24163 mbfres 24174 mbfimaopn2 24187 cncombf 24188 cnmbf 24189 0plef 24202 0pledm 24203 itg1ge0 24216 mbfi1fseqlem5 24249 itg2addlem 24288 limcfval 24399 limcrcl 24401 ellimc2 24404 limcflf 24408 limcres 24413 limcun 24422 dvfval 24424 dvbss 24428 dvbsss 24429 perfdvf 24430 dvreslem 24436 dvres2lem 24437 dvcnp2 24446 dvnfval 24448 dvnff 24449 dvnf 24453 dvnbss 24454 dvnadd 24455 dvn2bss 24456 dvnres 24457 cpnfval 24458 cpnord 24461 dvaddbr 24464 dvmulbr 24465 dvnfre 24478 dvexp 24479 dvef 24506 c1liplem1 24522 c1lip2 24524 lhop1lem 24539 plyval 24712 elply 24714 elply2 24715 plyf 24717 plyss 24718 elplyr 24720 plyeq0lem 24729 plyeq0 24730 plypf1 24731 plyaddlem1 24732 plymullem1 24733 plyaddlem 24734 plymullem 24735 plysub 24738 coeeulem 24743 coeeq 24746 dgrlem 24748 coeidlem 24756 plyco 24760 coe0 24775 coesub 24776 dgrmulc 24790 dgrsub 24791 dgrcolem1 24792 dgrcolem2 24793 plymul0or 24799 dvnply2 24805 plycpn 24807 plydivlem3 24813 plydivlem4 24814 plydiveu 24816 plyremlem 24822 plyrem 24823 facth 24824 fta1lem 24825 quotcan 24827 vieta1lem2 24829 plyexmo 24831 elqaalem3 24839 qaa 24841 iaa 24843 aannenlem1 24846 aannenlem2 24847 aannenlem3 24848 taylfvallem1 24874 taylfval 24876 tayl0 24879 taylplem1 24880 taylply2 24885 taylply 24886 dvtaylp 24887 dvntaylp 24888 dvntaylp0 24889 taylthlem1 24890 taylthlem2 24891 ulmval 24897 ulmss 24914 ulmcn 24916 mtest 24921 pserulm 24939 psercn 24943 pserdvlem2 24945 abelth 24958 reefgim 24967 cxpcn2 25254 logbmpt 25293 logbfval 25295 lgamgulmlem5 25538 lgamgulmlem6 25539 lgamgulm2 25541 lgamcvglem 25545 ftalem7 25584 dchrfi 25759 cffldtocusgr 27157 isvcOLD 28284 cnaddabloOLD 28286 cnnvg 28383 cnnvs 28385 cnnvnm 28386 cncph 28524 hvmulex 28716 hfsmval 29443 hfmmval 29444 nmfnval 29581 nlfnval 29586 elcnfn 29587 ellnfn 29588 specval 29603 hhcnf 29610 lmlim 31090 esumcvg 31245 plymul02 31716 plymulx0 31717 signsplypnf 31720 signsply0 31721 breprexplemb 31802 breprexpnat 31805 vtsval 31808 circlemethnat 31812 circlevma 31813 circlemethhgt 31814 cvxpconn 32387 fwddifval 33521 fwddifnval 33522 ivthALT 33581 knoppcnlem5 33734 knoppcnlem8 33737 bj-inftyexpiinv 34383 bj-inftyexpidisj 34385 caures 34918 cntotbnd 34957 cnpwstotbnd 34958 rrnval 34988 cnaddcom 35990 elmnc 39616 mpaaeu 39630 itgoval 39641 itgocn 39644 rngunsnply 39653 binomcxplemnotnn0 40568 climexp 41766 xlimbr 41988 fuzxrpmcn 41989 xlimmnfvlem2 41994 xlimpnfvlem2 41998 mulcncff 42031 subcncff 42043 addcncff 42047 cncfuni 42049 divcncff 42054 dvsinax 42077 dvcosax 42091 dvnmptdivc 42103 dvnmptconst 42106 dvnxpaek 42107 dvnmul 42108 dvnprodlem3 42113 etransclem1 42401 etransclem2 42402 etransclem4 42404 etransclem13 42413 etransclem46 42446 fdivpm 44501 amgmlemALT 44802 |
Copyright terms: Public domain | W3C validator |