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

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

Proof of Theorem cnex
StepHypRef Expression
1 ax-cnex 11085 1 ℂ ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2119  Vcvv 3431  cc 11027
This theorem was proved from axioms:  ax-cnex 11085
This theorem is referenced by:  reex  11120  cnelprrecn  11122  pnfex  11189  nnex  12171  zex  12524  qex  12902  mpoaddex  12929  addex  12930  mpomulex  12931  mulex  12932  rlim  15448  rlimf  15454  rlimss  15455  elo12  15480  o1f  15482  o1dm  15483  cnso  16205  cnaddablx  19834  cnaddabl  19835  cnaddid  19836  cnaddinv  19837  cnfldbas  21351  cnfldcj  21356  cnfldds  21359  cnfldfun  21361  cnfldfunALT  21362  cnmsubglem  21405  cnmsgngrp  21554  psgninv  21557  lmbrf  23243  lmfss  23279  lmres  23283  lmcnp  23287  cnmet  24754  cncfval  24873  elcncf  24874  cncfcnvcn  24910  cnheibor  24940  cnlmodlem1  25121  tcphex  25202  tchnmfval  25213  tcphcph  25222  lmmbr2  25244  lmmbrf  25247  iscau2  25262  iscauf  25265  caucfil  25268  cmetcaulem  25273  caussi  25282  causs  25283  lmclimf  25289  mbff  25610  ismbf  25613  ismbfcn  25614  mbfconst  25618  mbfres  25629  mbfimaopn2  25642  cncombf  25643  cnmbf  25644  0plef  25657  0pledm  25658  itg1ge0  25671  mbfi1fseqlem5  25704  itg2addlem  25743  limcfval  25857  limcrcl  25859  ellimc2  25862  limcflf  25866  limcres  25871  limcun  25880  dvfval  25882  dvbss  25886  dvbsss  25887  perfdvf  25888  dvreslem  25894  dvres2lem  25895  dvcnp2  25905  dvnfval  25907  dvnff  25908  dvnf  25912  dvnbss  25913  dvnadd  25914  dvn2bss  25915  dvnres  25916  cpnfval  25917  cpnord  25920  dvaddbr  25923  dvmulbr  25924  dvnfre  25937  dvexp  25938  dvef  25965  c1liplem1  25981  c1lip2  25983  lhop1lem  25998  plyval  26176  elply  26178  elply2  26179  plyf  26181  plyss  26182  elplyr  26184  plyeq0lem  26193  plyeq0  26194  plypf1  26195  plyaddlem1  26196  plymullem1  26197  plyaddlem  26198  plymullem  26199  plysub  26202  coeeulem  26207  coeeq  26210  dgrlem  26212  coeidlem  26220  plyco  26224  coe0  26239  coesub  26240  dgrmulc  26254  dgrsub  26255  dgrcolem1  26256  dgrcolem2  26257  plymul0or  26265  dvnply2  26271  plycpn  26273  plydivlem3  26279  plydivlem4  26280  plydiveu  26282  plyremlem  26288  plyrem  26289  facth  26290  fta1lem  26291  quotcan  26293  vieta1lem2  26295  plyexmo  26297  elqaalem3  26305  qaa  26307  iaa  26309  aannenlem1  26312  aannenlem2  26313  aannenlem3  26314  taylfvallem1  26340  taylfval  26342  tayl0  26345  taylplem1  26346  taylply2  26351  taylply  26352  dvtaylp  26353  dvntaylp  26354  dvntaylp0  26355  taylthlem1  26356  taylthlem2  26357  ulmval  26363  ulmss  26380  ulmcn  26382  mtest  26387  pserulm  26405  psercn  26409  pserdvlem2  26411  abelth  26424  reefgim  26433  cxpcn2  26728  logbmpt  26770  logbfval  26772  lgamgulmlem5  27014  lgamgulmlem6  27015  lgamgulm2  27017  lgamcvglem  27021  ftalem7  27060  dchrfi  27236  cffldtocusgr  29534  isvcOLD  30668  cnaddabloOLD  30670  cnnvg  30767  cnnvs  30769  cnnvnm  30770  cncph  30908  hvmulex  31100  hfsmval  31827  hfmmval  31828  nmfnval  31965  nlfnval  31970  elcnfn  31971  ellnfn  31972  specval  31987  hhcnf  31994  constrsuc  33922  lmlim  34131  esumcvg  34270  plymul02  34730  plymulx0  34731  signsplypnf  34734  signsply0  34735  breprexplemb  34815  breprexpnat  34818  vtsval  34821  circlemethnat  34825  circlevma  34826  circlemethhgt  34827  cvxpconn  35470  fwddifval  36390  fwddifnval  36391  ivthALT  36563  knoppcnlem5  36803  knoppcnlem8  36806  bj-inftyexpiinv  37568  bj-inftyexpidisj  37570  caures  38127  cntotbnd  38163  cnpwstotbnd  38164  rrnval  38194  cnaddcom  39464  subex  42731  absex  42732  cjex  42733  elmnc  43581  mpaaeu  43595  itgoval  43606  itgocn  43609  rngunsnply  43614  binomcxplemnotnn0  44800  climexp  46050  xlimbr  46270  fuzxrpmcn  46271  xlimmnfvlem2  46276  xlimpnfvlem2  46280  mulcncff  46313  subcncff  46323  addcncff  46327  cncfuni  46329  divcncff  46334  dvsinax  46356  dvcosax  46369  dvnmptdivc  46381  dvnmptconst  46384  dvnxpaek  46385  dvnmul  46386  dvnprodlem3  46391  etransclem1  46678  etransclem2  46679  etransclem4  46681  etransclem13  46690  etransclem46  46723  nthrucw  47331  cjnpoly  47352  fdivpm  49034  amgmlemALT  50293
  Copyright terms: Public domain W3C validator