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

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

Proof of Theorem cnex
StepHypRef Expression
1 ax-cnex 11166 1 ℂ ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  Vcvv 3475  cc 11108
This theorem was proved from axioms:  ax-cnex 11166
This theorem is referenced by:  reex  11201  cnelprrecn  11203  pnfex  11267  nnex  12218  zex  12567  qex  12945  addex  12972  mulex  12973  rlim  15439  rlimf  15445  rlimss  15446  elo12  15471  o1f  15473  o1dm  15474  cnso  16190  cnaddablx  19736  cnaddabl  19737  cnaddid  19738  cnaddinv  19739  cnfldbas  20948  cnfldcj  20951  cnfldds  20954  cnfldfun  20956  cnfldfunALT  20957  cnfldfunALTOLD  20958  cnmsubglem  21008  cnmsgngrp  21132  psgninv  21135  lmbrf  22764  lmfss  22800  lmres  22804  lmcnp  22808  cnmet  24288  cncfval  24404  elcncf  24405  cncfcnvcn  24441  cnheibor  24471  cnlmodlem1  24652  tcphex  24734  tchnmfval  24745  tcphcph  24754  lmmbr2  24776  lmmbrf  24779  iscau2  24794  iscauf  24797  caucfil  24800  cmetcaulem  24805  caussi  24814  causs  24815  lmclimf  24821  mbff  25142  ismbf  25145  ismbfcn  25146  mbfconst  25150  mbfres  25161  mbfimaopn2  25174  cncombf  25175  cnmbf  25176  0plef  25189  0pledm  25190  itg1ge0  25203  mbfi1fseqlem5  25237  itg2addlem  25276  limcfval  25389  limcrcl  25391  ellimc2  25394  limcflf  25398  limcres  25403  limcun  25412  dvfval  25414  dvbss  25418  dvbsss  25419  perfdvf  25420  dvreslem  25426  dvres2lem  25427  dvcnp2  25437  dvnfval  25439  dvnff  25440  dvnf  25444  dvnbss  25445  dvnadd  25446  dvn2bss  25447  dvnres  25448  cpnfval  25449  cpnord  25452  dvaddbr  25455  dvmulbr  25456  dvnfre  25469  dvexp  25470  dvef  25497  c1liplem1  25513  c1lip2  25515  lhop1lem  25530  plyval  25707  elply  25709  elply2  25710  plyf  25712  plyss  25713  elplyr  25715  plyeq0lem  25724  plyeq0  25725  plypf1  25726  plyaddlem1  25727  plymullem1  25728  plyaddlem  25729  plymullem  25730  plysub  25733  coeeulem  25738  coeeq  25741  dgrlem  25743  coeidlem  25751  plyco  25755  coe0  25770  coesub  25771  dgrmulc  25785  dgrsub  25786  dgrcolem1  25787  dgrcolem2  25788  plymul0or  25794  dvnply2  25800  plycpn  25802  plydivlem3  25808  plydivlem4  25809  plydiveu  25811  plyremlem  25817  plyrem  25818  facth  25819  fta1lem  25820  quotcan  25822  vieta1lem2  25824  plyexmo  25826  elqaalem3  25834  qaa  25836  iaa  25838  aannenlem1  25841  aannenlem2  25842  aannenlem3  25843  taylfvallem1  25869  taylfval  25871  tayl0  25874  taylplem1  25875  taylply2  25880  taylply  25881  dvtaylp  25882  dvntaylp  25883  dvntaylp0  25884  taylthlem1  25885  taylthlem2  25886  ulmval  25892  ulmss  25909  ulmcn  25911  mtest  25916  pserulm  25934  psercn  25938  pserdvlem2  25940  abelth  25953  reefgim  25962  cxpcn2  26254  logbmpt  26293  logbfval  26295  lgamgulmlem5  26537  lgamgulmlem6  26538  lgamgulm2  26540  lgamcvglem  26544  ftalem7  26583  dchrfi  26758  cffldtocusgr  28704  isvcOLD  29832  cnaddabloOLD  29834  cnnvg  29931  cnnvs  29933  cnnvnm  29934  cncph  30072  hvmulex  30264  hfsmval  30991  hfmmval  30992  nmfnval  31129  nlfnval  31134  elcnfn  31135  ellnfn  31136  specval  31151  hhcnf  31158  lmlim  32927  esumcvg  33084  plymul02  33557  plymulx0  33558  signsplypnf  33561  signsply0  33562  breprexplemb  33643  breprexpnat  33646  vtsval  33649  circlemethnat  33653  circlevma  33654  circlemethhgt  33655  cvxpconn  34233  fwddifval  35134  fwddifnval  35135  mpomulex  35161  gg-dvcnp2  35174  gg-dvmulbr  35175  ivthALT  35220  knoppcnlem5  35373  knoppcnlem8  35376  bj-inftyexpiinv  36089  bj-inftyexpidisj  36091  caures  36628  cntotbnd  36664  cnpwstotbnd  36665  rrnval  36695  cnaddcom  37842  elmnc  41878  mpaaeu  41892  itgoval  41903  itgocn  41906  rngunsnply  41915  binomcxplemnotnn0  43115  climexp  44321  xlimbr  44543  fuzxrpmcn  44544  xlimmnfvlem2  44549  xlimpnfvlem2  44553  mulcncff  44586  subcncff  44596  addcncff  44600  cncfuni  44602  divcncff  44607  dvsinax  44629  dvcosax  44642  dvnmptdivc  44654  dvnmptconst  44657  dvnxpaek  44658  dvnmul  44659  dvnprodlem3  44664  etransclem1  44951  etransclem2  44952  etransclem4  44954  etransclem13  44963  etransclem46  44996  fdivpm  47229  amgmlemALT  47850
  Copyright terms: Public domain W3C validator