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

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

Proof of Theorem cnex
StepHypRef Expression
1 ax-cnex 11152 1 ℂ ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2149  Vcvv 3463  cc 11094
This theorem was proved from axioms:  ax-cnex 11152
This theorem is referenced by:  reex  11187  cnelprrecn  11189  pnfex  11258  nnex  12235  zex  12596  qex  12981  mpoaddex  13008  addex  13009  mpomulex  13010  mulex  13011  rlim  15542  rlimf  15548  rlimss  15549  elo12  15574  o1f  15576  o1dm  15577  cnso  16299  cnaddablx  19934  cnaddabl  19935  cnaddid  19936  cnaddinv  19937  cnfldbas  21491  cnfldcj  21496  cnfldds  21499  cnfldfun  21501  cnfldfunALT  21502  cnmsubglem  21545  cnmsgngrp  21694  psgninv  21697  lmbrf  23382  lmfss  23418  lmres  23422  lmcnp  23426  cnmet  24893  cncfval  25012  elcncf  25013  cncfcnvcn  25049  cnheibor  25079  cnlmodlem1  25260  tcphex  25341  tchnmfval  25352  tcphcph  25361  lmmbr2  25383  lmmbrf  25386  iscau2  25401  iscauf  25404  caucfil  25407  cmetcaulem  25412  caussi  25421  causs  25422  lmclimf  25428  mbff  25749  ismbf  25752  ismbfcn  25753  mbfconst  25757  mbfres  25768  mbfimaopn2  25781  cncombf  25782  cnmbf  25783  0plef  25796  0pledm  25797  itg1ge0  25810  mbfi1fseqlem5  25843  itg2addlem  25882  limcfval  25996  limcrcl  25998  ellimc2  26001  limcflf  26005  limcres  26010  limcun  26019  dvfval  26021  dvbss  26025  dvbsss  26026  perfdvf  26027  dvreslem  26033  dvres2lem  26034  dvcnp2  26044  dvnfval  26046  dvnff  26047  dvnf  26051  dvnbss  26052  dvnadd  26053  dvn2bss  26054  dvnres  26055  cpnfval  26056  cpnord  26059  dvaddbr  26062  dvmulbr  26063  dvnfre  26076  dvexp  26077  dvef  26104  c1liplem1  26120  c1lip2  26122  lhop1lem  26137  plyval  26315  elply  26317  elply2  26318  plyf  26320  plyss  26321  elplyr  26323  plyeq0lem  26332  plyeq0  26333  plypf1  26334  plyaddlem1  26335  plymullem1  26336  plyaddlem  26337  plymullem  26338  plysub  26341  coeeulem  26346  coeeq  26349  dgrlem  26351  coeidlem  26359  plyco  26363  coe0  26378  coesub  26379  dgrmulc  26393  dgrsub  26394  dgrcolem1  26395  dgrcolem2  26396  plymul0or  26404  plymul02  26406  plyn0mulidp  26407  dvnply2  26413  plycpn  26415  plydivlem3  26421  plydivlem4  26422  plydiveu  26424  plyremlem  26430  plyrem  26431  facth  26432  fta1lem  26433  quotcan  26435  vieta1lem2  26437  plyexmo  26439  elqaalem3  26447  qaa  26449  iaa  26451  aannenlem1  26454  aannenlem2  26455  aannenlem3  26456  taylfvallem1  26482  taylfval  26484  tayl0  26487  taylplem1  26488  taylply2  26493  taylply  26494  dvtaylp  26495  dvntaylp  26496  dvntaylp0  26497  taylthlem1  26498  taylthlem2  26499  ulmval  26505  ulmss  26522  ulmcn  26524  mtest  26529  pserulm  26547  psercn  26551  pserdvlem2  26553  abelth  26566  reefgim  26575  cxpcn2  26873  logbmpt  26915  logbfval  26917  lgamgulmlem5  27159  lgamgulmlem6  27160  lgamgulm2  27162  lgamcvglem  27166  ftalem7  27205  dchrfi  27381  cffldtocusgr  29734  isvcOLD  30868  cnaddabloOLD  30870  cnnvg  30967  cnnvs  30969  cnnvnm  30970  cncph  31108  hvmulex  31300  hfsmval  32027  hfmmval  32028  nmfnval  32165  nlfnval  32170  elcnfn  32171  ellnfn  32172  specval  32187  hhcnf  32194  constrsuc  34069  lmlim  34278  esumcvg  34417  signsplypnf  34878  signsply0  34879  breprexplemb  34959  breprexpnat  34962  vtsval  34965  circlemethnat  34969  circlevma  34970  circlemethhgt  34971  cvxpconn  35629  fwddifval  36549  fwddifnval  36550  ivthALT  36731  knoppcnlem5  36971  knoppcnlem8  36974  bj-inftyexpiinv  37735  bj-inftyexpidisj  37737  caures  38294  cntotbnd  38330  cnpwstotbnd  38331  rrnval  38361  cnaddcom  39631  subex  42898  absex  42899  cjex  42900  elmnc  43748  mpaaeu  43762  itgoval  43773  itgocn  43776  rngunsnply  43781  binomcxplemnotnn0  44951  climexp  46206  xlimbr  46426  fuzxrpmcn  46427  xlimmnfvlem2  46432  xlimpnfvlem2  46436  mulcncff  46469  subcncff  46479  addcncff  46483  cncfuni  46485  divcncff  46490  dvsinax  46512  dvcosax  46525  dvnmptdivc  46537  dvnmptconst  46540  dvnxpaek  46541  dvnmul  46542  dvnprodlem3  46547  etransclem1  46834  etransclem2  46835  etransclem4  46837  etransclem13  46846  etransclem46  46879  nthrucw  47487  cjnpoly  47508  fdivpm  49201  amgmlemALT  50459
  Copyright terms: Public domain W3C validator