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

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

Proof of Theorem cnex
StepHypRef 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