MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cnex Structured version   Visualization version   GIF version

Theorem cnex 11119
Description: Alias for ax-cnex 11094. See also cnexALT 12936. (Contributed by Mario Carneiro, 17-Nov-2014.)
Assertion
Ref Expression
cnex ℂ ∈ V

Proof of Theorem cnex
StepHypRef Expression
1 ax-cnex 11094 1 ℂ ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2114  Vcvv 3429  cc 11036
This theorem was proved from axioms:  ax-cnex 11094
This theorem is referenced by:  reex  11129  cnelprrecn  11131  pnfex  11198  nnex  12180  zex  12533  qex  12911  mpoaddex  12938  addex  12939  mpomulex  12940  mulex  12941  rlim  15457  rlimf  15463  rlimss  15464  elo12  15489  o1f  15491  o1dm  15492  cnso  16214  cnaddablx  19843  cnaddabl  19844  cnaddid  19845  cnaddinv  19846  cnfldbas  21356  cnfldcj  21361  cnfldds  21364  cnfldfun  21366  cnfldfunALT  21367  cnmsubglem  21410  cnmsgngrp  21559  psgninv  21562  lmbrf  23225  lmfss  23261  lmres  23265  lmcnp  23269  cnmet  24736  cncfval  24855  elcncf  24856  cncfcnvcn  24892  cnheibor  24922  cnlmodlem1  25103  tcphex  25184  tchnmfval  25195  tcphcph  25204  lmmbr2  25226  lmmbrf  25229  iscau2  25244  iscauf  25247  caucfil  25250  cmetcaulem  25255  caussi  25264  causs  25265  lmclimf  25271  mbff  25592  ismbf  25595  ismbfcn  25596  mbfconst  25600  mbfres  25611  mbfimaopn2  25624  cncombf  25625  cnmbf  25626  0plef  25639  0pledm  25640  itg1ge0  25653  mbfi1fseqlem5  25686  itg2addlem  25725  limcfval  25839  limcrcl  25841  ellimc2  25844  limcflf  25848  limcres  25853  limcun  25862  dvfval  25864  dvbss  25868  dvbsss  25869  perfdvf  25870  dvreslem  25876  dvres2lem  25877  dvcnp2  25887  dvnfval  25889  dvnff  25890  dvnf  25894  dvnbss  25895  dvnadd  25896  dvn2bss  25897  dvnres  25898  cpnfval  25899  cpnord  25902  dvaddbr  25905  dvmulbr  25906  dvnfre  25919  dvexp  25920  dvef  25947  c1liplem1  25963  c1lip2  25965  lhop1lem  25980  plyval  26158  elply  26160  elply2  26161  plyf  26163  plyss  26164  elplyr  26166  plyeq0lem  26175  plyeq0  26176  plypf1  26177  plyaddlem1  26178  plymullem1  26179  plyaddlem  26180  plymullem  26181  plysub  26184  coeeulem  26189  coeeq  26192  dgrlem  26194  coeidlem  26202  plyco  26206  coe0  26221  coesub  26222  dgrmulc  26236  dgrsub  26237  dgrcolem1  26238  dgrcolem2  26239  plymul0or  26247  dvnply2  26253  plycpn  26255  plydivlem3  26261  plydivlem4  26262  plydiveu  26264  plyremlem  26270  plyrem  26271  facth  26272  fta1lem  26273  quotcan  26275  vieta1lem2  26277  plyexmo  26279  elqaalem3  26287  qaa  26289  iaa  26291  aannenlem1  26294  aannenlem2  26295  aannenlem3  26296  taylfvallem1  26322  taylfval  26324  tayl0  26327  taylplem1  26328  taylply2  26333  taylply  26334  dvtaylp  26335  dvntaylp  26336  dvntaylp0  26337  taylthlem1  26338  taylthlem2  26339  ulmval  26345  ulmss  26362  ulmcn  26364  mtest  26369  pserulm  26387  psercn  26391  pserdvlem2  26393  abelth  26406  reefgim  26415  cxpcn2  26710  logbmpt  26752  logbfval  26754  lgamgulmlem5  26996  lgamgulmlem6  26997  lgamgulm2  26999  lgamcvglem  27003  ftalem7  27042  dchrfi  27218  cffldtocusgr  29516  isvcOLD  30650  cnaddabloOLD  30652  cnnvg  30749  cnnvs  30751  cnnvnm  30752  cncph  30890  hvmulex  31082  hfsmval  31809  hfmmval  31810  nmfnval  31947  nlfnval  31952  elcnfn  31953  ellnfn  31954  specval  31969  hhcnf  31976  constrsuc  33882  lmlim  34091  esumcvg  34230  plymul02  34690  plymulx0  34691  signsplypnf  34694  signsply0  34695  breprexplemb  34775  breprexpnat  34778  vtsval  34781  circlemethnat  34785  circlevma  34786  circlemethhgt  34787  cvxpconn  35424  fwddifval  36344  fwddifnval  36345  ivthALT  36517  knoppcnlem5  36757  knoppcnlem8  36760  bj-inftyexpiinv  37522  bj-inftyexpidisj  37524  caures  38081  cntotbnd  38117  cnpwstotbnd  38118  rrnval  38148  cnaddcom  39418  subex  42686  absex  42687  cjex  42688  elmnc  43564  mpaaeu  43578  itgoval  43589  itgocn  43592  rngunsnply  43597  binomcxplemnotnn0  44783  climexp  46035  xlimbr  46255  fuzxrpmcn  46256  xlimmnfvlem2  46261  xlimpnfvlem2  46265  mulcncff  46298  subcncff  46308  addcncff  46312  cncfuni  46314  divcncff  46319  dvsinax  46341  dvcosax  46354  dvnmptdivc  46366  dvnmptconst  46369  dvnxpaek  46370  dvnmul  46371  dvnprodlem3  46376  etransclem1  46663  etransclem2  46664  etransclem4  46666  etransclem13  46675  etransclem46  46708  nthrucw  47316  cjnpoly  47337  fdivpm  49019  amgmlemALT  50278
  Copyright terms: Public domain W3C validator