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

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

Proof of Theorem cnex
StepHypRef Expression
1 ax-cnex 11116 1 ℂ ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2106  Vcvv 3446  cc 11058
This theorem was proved from axioms:  ax-cnex 11116
This theorem is referenced by:  reex  11151  cnelprrecn  11153  pnfex  11217  nnex  12168  zex  12517  qex  12895  addex  12922  mulex  12923  rlim  15389  rlimf  15395  rlimss  15396  elo12  15421  o1f  15423  o1dm  15424  cnso  16140  cnaddablx  19660  cnaddabl  19661  cnaddid  19662  cnaddinv  19663  cnfldbas  20837  cnfldcj  20840  cnfldds  20843  cnfldfun  20845  cnfldfunALT  20846  cnfldfunALTOLD  20847  cnmsubglem  20897  cnmsgngrp  21020  psgninv  21023  lmbrf  22648  lmfss  22684  lmres  22688  lmcnp  22692  cnmet  24172  cncfval  24288  elcncf  24289  cncfcnvcn  24325  cnheibor  24355  cnlmodlem1  24536  tcphex  24618  tchnmfval  24629  tcphcph  24638  lmmbr2  24660  lmmbrf  24663  iscau2  24678  iscauf  24681  caucfil  24684  cmetcaulem  24689  caussi  24698  causs  24699  lmclimf  24705  mbff  25026  ismbf  25029  ismbfcn  25030  mbfconst  25034  mbfres  25045  mbfimaopn2  25058  cncombf  25059  cnmbf  25060  0plef  25073  0pledm  25074  itg1ge0  25087  mbfi1fseqlem5  25121  itg2addlem  25160  limcfval  25273  limcrcl  25275  ellimc2  25278  limcflf  25282  limcres  25287  limcun  25296  dvfval  25298  dvbss  25302  dvbsss  25303  perfdvf  25304  dvreslem  25310  dvres2lem  25311  dvcnp2  25321  dvnfval  25323  dvnff  25324  dvnf  25328  dvnbss  25329  dvnadd  25330  dvn2bss  25331  dvnres  25332  cpnfval  25333  cpnord  25336  dvaddbr  25339  dvmulbr  25340  dvnfre  25353  dvexp  25354  dvef  25381  c1liplem1  25397  c1lip2  25399  lhop1lem  25414  plyval  25591  elply  25593  elply2  25594  plyf  25596  plyss  25597  elplyr  25599  plyeq0lem  25608  plyeq0  25609  plypf1  25610  plyaddlem1  25611  plymullem1  25612  plyaddlem  25613  plymullem  25614  plysub  25617  coeeulem  25622  coeeq  25625  dgrlem  25627  coeidlem  25635  plyco  25639  coe0  25654  coesub  25655  dgrmulc  25669  dgrsub  25670  dgrcolem1  25671  dgrcolem2  25672  plymul0or  25678  dvnply2  25684  plycpn  25686  plydivlem3  25692  plydivlem4  25693  plydiveu  25695  plyremlem  25701  plyrem  25702  facth  25703  fta1lem  25704  quotcan  25706  vieta1lem2  25708  plyexmo  25710  elqaalem3  25718  qaa  25720  iaa  25722  aannenlem1  25725  aannenlem2  25726  aannenlem3  25727  taylfvallem1  25753  taylfval  25755  tayl0  25758  taylplem1  25759  taylply2  25764  taylply  25765  dvtaylp  25766  dvntaylp  25767  dvntaylp0  25768  taylthlem1  25769  taylthlem2  25770  ulmval  25776  ulmss  25793  ulmcn  25795  mtest  25800  pserulm  25818  psercn  25822  pserdvlem2  25824  abelth  25837  reefgim  25846  cxpcn2  26136  logbmpt  26175  logbfval  26177  lgamgulmlem5  26419  lgamgulmlem6  26420  lgamgulm2  26422  lgamcvglem  26426  ftalem7  26465  dchrfi  26640  cffldtocusgr  28458  isvcOLD  29584  cnaddabloOLD  29586  cnnvg  29683  cnnvs  29685  cnnvnm  29686  cncph  29824  hvmulex  30016  hfsmval  30743  hfmmval  30744  nmfnval  30881  nlfnval  30886  elcnfn  30887  ellnfn  30888  specval  30903  hhcnf  30910  lmlim  32617  esumcvg  32774  plymul02  33247  plymulx0  33248  signsplypnf  33251  signsply0  33252  breprexplemb  33333  breprexpnat  33336  vtsval  33339  circlemethnat  33343  circlevma  33344  circlemethhgt  33345  cvxpconn  33923  fwddifval  34823  fwddifnval  34824  ivthALT  34883  knoppcnlem5  35036  knoppcnlem8  35039  bj-inftyexpiinv  35752  bj-inftyexpidisj  35754  caures  36292  cntotbnd  36328  cnpwstotbnd  36329  rrnval  36359  cnaddcom  37507  elmnc  41521  mpaaeu  41535  itgoval  41546  itgocn  41549  rngunsnply  41558  binomcxplemnotnn0  42758  climexp  43966  xlimbr  44188  fuzxrpmcn  44189  xlimmnfvlem2  44194  xlimpnfvlem2  44198  mulcncff  44231  subcncff  44241  addcncff  44245  cncfuni  44247  divcncff  44252  dvsinax  44274  dvcosax  44287  dvnmptdivc  44299  dvnmptconst  44302  dvnxpaek  44303  dvnmul  44304  dvnprodlem3  44309  etransclem1  44596  etransclem2  44597  etransclem4  44599  etransclem13  44608  etransclem46  44641  fdivpm  46749  amgmlemALT  47370
  Copyright terms: Public domain W3C validator