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

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

Proof of Theorem cnex
StepHypRef Expression
1 ax-cnex 11084 1 ℂ ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2109  Vcvv 3438  cc 11026
This theorem was proved from axioms:  ax-cnex 11084
This theorem is referenced by:  reex  11119  cnelprrecn  11121  pnfex  11187  nnex  12152  zex  12498  qex  12880  mpoaddex  12907  addex  12908  mpomulex  12909  mulex  12910  rlim  15420  rlimf  15426  rlimss  15427  elo12  15452  o1f  15454  o1dm  15455  cnso  16174  cnaddablx  19765  cnaddabl  19766  cnaddid  19767  cnaddinv  19768  cnfldbas  21283  cnfldcj  21288  cnfldds  21291  cnfldfun  21293  cnfldfunALT  21294  cnfldbasOLD  21298  cnfldcjOLD  21301  cnflddsOLD  21304  cnfldfunOLD  21306  cnfldfunALTOLD  21307  cnmsubglem  21355  cnmsgngrp  21504  psgninv  21507  lmbrf  23163  lmfss  23199  lmres  23203  lmcnp  23207  cnmet  24675  cncfval  24797  elcncf  24798  cncfcnvcn  24835  cnheibor  24870  cnlmodlem1  25052  tcphex  25133  tchnmfval  25144  tcphcph  25153  lmmbr2  25175  lmmbrf  25178  iscau2  25193  iscauf  25196  caucfil  25199  cmetcaulem  25204  caussi  25213  causs  25214  lmclimf  25220  mbff  25542  ismbf  25545  ismbfcn  25546  mbfconst  25550  mbfres  25561  mbfimaopn2  25574  cncombf  25575  cnmbf  25576  0plef  25589  0pledm  25590  itg1ge0  25603  mbfi1fseqlem5  25636  itg2addlem  25675  limcfval  25789  limcrcl  25791  ellimc2  25794  limcflf  25798  limcres  25803  limcun  25812  dvfval  25814  dvbss  25818  dvbsss  25819  perfdvf  25820  dvreslem  25826  dvres2lem  25827  dvcnp2  25837  dvcnp2OLD  25838  dvnfval  25840  dvnff  25841  dvnf  25845  dvnbss  25846  dvnadd  25847  dvn2bss  25848  dvnres  25849  cpnfval  25850  cpnord  25853  dvaddbr  25856  dvmulbr  25857  dvmulbrOLD  25858  dvnfre  25872  dvexp  25873  dvef  25900  c1liplem1  25917  c1lip2  25919  lhop1lem  25934  plyval  26114  elply  26116  elply2  26117  plyf  26119  plyss  26120  elplyr  26122  plyeq0lem  26131  plyeq0  26132  plypf1  26133  plyaddlem1  26134  plymullem1  26135  plyaddlem  26136  plymullem  26137  plysub  26140  coeeulem  26145  coeeq  26148  dgrlem  26150  coeidlem  26158  plyco  26162  coe0  26177  coesub  26178  dgrmulc  26193  dgrsub  26194  dgrcolem1  26195  dgrcolem2  26196  plymul0or  26204  dvnply2  26211  plycpn  26213  plydivlem3  26219  plydivlem4  26220  plydiveu  26222  plyremlem  26228  plyrem  26229  facth  26230  fta1lem  26231  quotcan  26233  vieta1lem2  26235  plyexmo  26237  elqaalem3  26245  qaa  26247  iaa  26249  aannenlem1  26252  aannenlem2  26253  aannenlem3  26254  taylfvallem1  26280  taylfval  26282  tayl0  26285  taylplem1  26286  taylply2  26291  taylply2OLD  26292  taylply  26293  dvtaylp  26294  dvntaylp  26295  dvntaylp0  26296  taylthlem1  26297  taylthlem2  26298  taylthlem2OLD  26299  ulmval  26305  ulmss  26322  ulmcn  26324  mtest  26329  pserulm  26347  psercn  26352  pserdvlem2  26354  abelth  26367  reefgim  26376  cxpcn2  26672  logbmpt  26714  logbfval  26716  lgamgulmlem5  26959  lgamgulmlem6  26960  lgamgulm2  26962  lgamcvglem  26966  ftalem7  27005  dchrfi  27182  cffldtocusgr  29410  cffldtocusgrOLD  29411  isvcOLD  30541  cnaddabloOLD  30543  cnnvg  30640  cnnvs  30642  cnnvnm  30643  cncph  30781  hvmulex  30973  hfsmval  31700  hfmmval  31701  nmfnval  31838  nlfnval  31843  elcnfn  31844  ellnfn  31845  specval  31860  hhcnf  31867  constrsuc  33707  lmlim  33916  esumcvg  34055  plymul02  34516  plymulx0  34517  signsplypnf  34520  signsply0  34521  breprexplemb  34601  breprexpnat  34604  vtsval  34607  circlemethnat  34611  circlevma  34612  circlemethhgt  34613  cvxpconn  35217  fwddifval  36138  fwddifnval  36139  ivthALT  36311  knoppcnlem5  36473  knoppcnlem8  36476  bj-inftyexpiinv  37184  bj-inftyexpidisj  37186  caures  37742  cntotbnd  37778  cnpwstotbnd  37779  rrnval  37809  cnaddcom  38953  subex  42223  absex  42224  cjex  42225  elmnc  43112  mpaaeu  43126  itgoval  43137  itgocn  43140  rngunsnply  43145  binomcxplemnotnn0  44332  climexp  45590  xlimbr  45812  fuzxrpmcn  45813  xlimmnfvlem2  45818  xlimpnfvlem2  45822  mulcncff  45855  subcncff  45865  addcncff  45869  cncfuni  45871  divcncff  45876  dvsinax  45898  dvcosax  45911  dvnmptdivc  45923  dvnmptconst  45926  dvnxpaek  45927  dvnmul  45928  dvnprodlem3  45933  etransclem1  46220  etransclem2  46221  etransclem4  46223  etransclem13  46232  etransclem46  46265  cjnpoly  46877  fdivpm  48532  amgmlemALT  49792
  Copyright terms: Public domain W3C validator