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

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

Proof of Theorem cnex
StepHypRef Expression
1 ax-cnex 10215 1 ℂ ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2148  Vcvv 3355  cc 10157
This theorem was proved from axioms:  ax-cnex 10215
This theorem is referenced by:  reex  10250  cnelprrecn  10252  pnfxr  10315  nnex  11249  zex  11610  qex  12025  addex  12050  mulex  12051  rlim  14456  rlimf  14462  rlimss  14463  elo12  14488  o1f  14490  o1dm  14491  cnso  15204  cnaddablx  18498  cnaddabl  18499  cnaddid  18500  cnaddinv  18501  cnfldbas  19985  cnfldcj  19988  cnfldds  19991  cnfldfun  19993  cnfldfunALT  19994  cnmsubglem  20044  cnmsgngrp  20160  psgninv  20163  lmbrf  21305  lmfss  21341  lmres  21345  lmcnp  21349  cnmet  22815  cncfval  22931  elcncf  22932  cncfcnvcn  22964  cnheibor  22994  cnlmodlem1  23175  tchex  23255  tchnmfval  23266  tchcph  23275  lmmbr2  23296  lmmbrf  23299  iscau2  23314  iscauf  23317  caucfil  23320  cmetcaulem  23325  caussi  23334  causs  23335  lmclimf  23341  mbff  23633  ismbf  23636  ismbfcn  23637  mbfconst  23641  mbfres  23652  mbfimaopn2  23665  cncombf  23666  cnmbf  23667  0plef  23680  0pledm  23681  itg1ge0  23694  mbfi1fseqlem5  23727  itg2addlem  23766  limcfval  23877  limcrcl  23879  ellimc2  23882  limcflf  23886  limcres  23891  limcun  23900  dvfval  23902  dvbss  23906  dvbsss  23907  perfdvf  23908  dvreslem  23914  dvres2lem  23915  dvcnp2  23924  dvnfval  23926  dvnff  23927  dvnf  23931  dvnbss  23932  dvnadd  23933  dvn2bss  23934  dvnres  23935  cpnfval  23936  cpnord  23939  dvaddbr  23942  dvmulbr  23943  dvnfre  23956  dvexp  23957  dvef  23984  c1liplem1  24000  c1lip2  24002  lhop1lem  24017  plyval  24190  elply  24192  elply2  24193  plyf  24195  plyss  24196  elplyr  24198  plyeq0lem  24207  plyeq0  24208  plypf1  24209  plyaddlem1  24210  plymullem1  24211  plyaddlem  24212  plymullem  24213  plysub  24216  coeeulem  24221  coeeq  24224  dgrlem  24226  coeidlem  24234  plyco  24238  coe0  24253  coesub  24254  dgrmulc  24268  dgrsub  24269  dgrcolem1  24270  dgrcolem2  24271  plymul0or  24277  dvnply2  24283  plycpn  24285  plydivlem3  24291  plydivlem4  24292  plydiveu  24294  plyremlem  24300  plyrem  24301  facth  24302  fta1lem  24303  quotcan  24305  vieta1lem2  24307  plyexmo  24309  elqaalem3  24317  qaa  24319  iaa  24321  aannenlem1  24324  aannenlem2  24325  aannenlem3  24326  taylfvallem1  24352  taylfval  24354  tayl0  24357  taylplem1  24358  taylply2  24363  taylply  24364  dvtaylp  24365  dvntaylp  24366  dvntaylp0  24367  taylthlem1  24368  taylthlem2  24369  ulmval  24375  ulmss  24392  ulmcn  24394  mtest  24399  pserulm  24417  psercn  24421  pserdvlem2  24423  abelth  24436  reefgim  24445  cxpcn2  24729  logbmpt  24768  logbfval  24770  lgamgulmlem5  25001  lgamgulmlem6  25002  lgamgulm2  25004  lgamcvglem  25008  ftalem7  25047  dchrfi  25222  cffldtocusgr  26599  isvcOLD  27791  cnaddabloOLD  27793  cnnvg  27890  cnnvs  27892  cnnvnm  27893  cncph  28031  hvmulex  28225  hfsmval  28954  hfmmval  28955  nmfnval  29092  nlfnval  29097  elcnfn  29098  ellnfn  29099  specval  29114  hhcnf  29121  lmlim  30350  esumcvg  30505  plymul02  30980  plymulx0  30981  signsplypnf  30984  signsply0  30985  breprexplemb  31066  breprexpnat  31069  vtsval  31072  circlemethnat  31076  circlevma  31077  circlemethhgt  31078  cvxpconn  31579  fwddifval  32623  fwddifnval  32624  ivthALT  32684  knoppcnlem5  32841  knoppcnlem8  32844  bj-inftyexpiinv  33449  bj-inftyexpidisj  33451  caures  33904  cntotbnd  33943  cnpwstotbnd  33944  rrnval  33974  cnaddcom  34796  elmnc  38247  mpaaeu  38261  itgoval  38272  itgocn  38275  rngunsnply  38284  binomcxplemnotnn0  39095  climexp  40361  xlimbr  40577  fuzxrpmcn  40578  xlimmnfvlem2  40583  xlimpnfvlem2  40587  mulcncff  40605  subcncff  40617  addcncff  40621  cncfuni  40623  divcncff  40628  dvsinax  40651  dvcosax  40665  dvnmptdivc  40677  dvnmptconst  40680  dvnxpaek  40681  dvnmul  40682  dvnprodlem3  40687  etransclem1  40975  etransclem2  40976  etransclem4  40978  etransclem13  40987  etransclem46  41020  fdivpm  42889  amgmlemALT  43104
  Copyright terms: Public domain W3C validator