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 2114  Vcvv 3430  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  21348  cnfldcj  21353  cnfldds  21356  cnfldfun  21358  cnfldfunALT  21359  cnfldbasOLD  21363  cnfldcjOLD  21366  cnflddsOLD  21369  cnfldfunOLD  21371  cnfldfunALTOLD  21372  cnmsubglem  21420  cnmsgngrp  21569  psgninv  21572  lmbrf  23235  lmfss  23271  lmres  23275  lmcnp  23279  cnmet  24746  cncfval  24865  elcncf  24866  cncfcnvcn  24902  cnheibor  24932  cnlmodlem1  25113  tcphex  25194  tchnmfval  25205  tcphcph  25214  lmmbr2  25236  lmmbrf  25239  iscau2  25254  iscauf  25257  caucfil  25260  cmetcaulem  25265  caussi  25274  causs  25275  lmclimf  25281  mbff  25602  ismbf  25605  ismbfcn  25606  mbfconst  25610  mbfres  25621  mbfimaopn2  25634  cncombf  25635  cnmbf  25636  0plef  25649  0pledm  25650  itg1ge0  25663  mbfi1fseqlem5  25696  itg2addlem  25735  limcfval  25849  limcrcl  25851  ellimc2  25854  limcflf  25858  limcres  25863  limcun  25872  dvfval  25874  dvbss  25878  dvbsss  25879  perfdvf  25880  dvreslem  25886  dvres2lem  25887  dvcnp2  25897  dvnfval  25899  dvnff  25900  dvnf  25904  dvnbss  25905  dvnadd  25906  dvn2bss  25907  dvnres  25908  cpnfval  25909  cpnord  25912  dvaddbr  25915  dvmulbr  25916  dvnfre  25929  dvexp  25930  dvef  25957  c1liplem1  25973  c1lip2  25975  lhop1lem  25990  plyval  26168  elply  26170  elply2  26171  plyf  26173  plyss  26174  elplyr  26176  plyeq0lem  26185  plyeq0  26186  plypf1  26187  plyaddlem1  26188  plymullem1  26189  plyaddlem  26190  plymullem  26191  plysub  26194  coeeulem  26199  coeeq  26202  dgrlem  26204  coeidlem  26212  plyco  26216  coe0  26231  coesub  26232  dgrmulc  26246  dgrsub  26247  dgrcolem1  26248  dgrcolem2  26249  plymul0or  26257  dvnply2  26264  plycpn  26266  plydivlem3  26272  plydivlem4  26273  plydiveu  26275  plyremlem  26281  plyrem  26282  facth  26283  fta1lem  26284  quotcan  26286  vieta1lem2  26288  plyexmo  26290  elqaalem3  26298  qaa  26300  iaa  26302  aannenlem1  26305  aannenlem2  26306  aannenlem3  26307  taylfvallem1  26333  taylfval  26335  tayl0  26338  taylplem1  26339  taylply2  26344  taylply2OLD  26345  taylply  26346  dvtaylp  26347  dvntaylp  26348  dvntaylp0  26349  taylthlem1  26350  taylthlem2  26351  taylthlem2OLD  26352  ulmval  26358  ulmss  26375  ulmcn  26377  mtest  26382  pserulm  26400  psercn  26404  pserdvlem2  26406  abelth  26419  reefgim  26428  cxpcn2  26723  logbmpt  26765  logbfval  26767  lgamgulmlem5  27010  lgamgulmlem6  27011  lgamgulm2  27013  lgamcvglem  27017  ftalem7  27056  dchrfi  27232  cffldtocusgr  29530  cffldtocusgrOLD  29531  isvcOLD  30665  cnaddabloOLD  30667  cnnvg  30764  cnnvs  30766  cnnvnm  30767  cncph  30905  hvmulex  31097  hfsmval  31824  hfmmval  31825  nmfnval  31962  nlfnval  31967  elcnfn  31968  ellnfn  31969  specval  31984  hhcnf  31991  constrsuc  33898  lmlim  34107  esumcvg  34246  plymul02  34706  plymulx0  34707  signsplypnf  34710  signsply0  34711  breprexplemb  34791  breprexpnat  34794  vtsval  34797  circlemethnat  34801  circlevma  34802  circlemethhgt  34803  cvxpconn  35440  fwddifval  36360  fwddifnval  36361  ivthALT  36533  knoppcnlem5  36773  knoppcnlem8  36776  bj-inftyexpiinv  37538  bj-inftyexpidisj  37540  caures  38095  cntotbnd  38131  cnpwstotbnd  38132  rrnval  38162  cnaddcom  39432  subex  42700  absex  42701  cjex  42702  elmnc  43582  mpaaeu  43596  itgoval  43607  itgocn  43610  rngunsnply  43615  binomcxplemnotnn0  44801  climexp  46053  xlimbr  46273  fuzxrpmcn  46274  xlimmnfvlem2  46279  xlimpnfvlem2  46283  mulcncff  46316  subcncff  46326  addcncff  46330  cncfuni  46332  divcncff  46337  dvsinax  46359  dvcosax  46372  dvnmptdivc  46384  dvnmptconst  46387  dvnxpaek  46388  dvnmul  46389  dvnprodlem3  46394  etransclem1  46681  etransclem2  46682  etransclem4  46684  etransclem13  46693  etransclem46  46726  nthrucw  47332  cjnpoly  47349  fdivpm  49031  amgmlemALT  50290
  Copyright terms: Public domain W3C validator