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

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

Proof of Theorem cnex
StepHypRef Expression
1 ax-cnex 10927 1 ℂ ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2106  Vcvv 3432  cc 10869
This theorem was proved from axioms:  ax-cnex 10927
This theorem is referenced by:  reex  10962  cnelprrecn  10964  pnfex  11028  nnex  11979  zex  12328  qex  12701  addex  12728  mulex  12729  rlim  15204  rlimf  15210  rlimss  15211  elo12  15236  o1f  15238  o1dm  15239  cnso  15956  cnaddablx  19469  cnaddabl  19470  cnaddid  19471  cnaddinv  19472  cnfldbas  20601  cnfldcj  20604  cnfldds  20607  cnfldfun  20609  cnfldfunALT  20610  cnfldfunALTOLD  20611  cnmsubglem  20661  cnmsgngrp  20784  psgninv  20787  lmbrf  22411  lmfss  22447  lmres  22451  lmcnp  22455  cnmet  23935  cncfval  24051  elcncf  24052  cncfcnvcn  24088  cnheibor  24118  cnlmodlem1  24299  tcphex  24381  tchnmfval  24392  tcphcph  24401  lmmbr2  24423  lmmbrf  24426  iscau2  24441  iscauf  24444  caucfil  24447  cmetcaulem  24452  caussi  24461  causs  24462  lmclimf  24468  mbff  24789  ismbf  24792  ismbfcn  24793  mbfconst  24797  mbfres  24808  mbfimaopn2  24821  cncombf  24822  cnmbf  24823  0plef  24836  0pledm  24837  itg1ge0  24850  mbfi1fseqlem5  24884  itg2addlem  24923  limcfval  25036  limcrcl  25038  ellimc2  25041  limcflf  25045  limcres  25050  limcun  25059  dvfval  25061  dvbss  25065  dvbsss  25066  perfdvf  25067  dvreslem  25073  dvres2lem  25074  dvcnp2  25084  dvnfval  25086  dvnff  25087  dvnf  25091  dvnbss  25092  dvnadd  25093  dvn2bss  25094  dvnres  25095  cpnfval  25096  cpnord  25099  dvaddbr  25102  dvmulbr  25103  dvnfre  25116  dvexp  25117  dvef  25144  c1liplem1  25160  c1lip2  25162  lhop1lem  25177  plyval  25354  elply  25356  elply2  25357  plyf  25359  plyss  25360  elplyr  25362  plyeq0lem  25371  plyeq0  25372  plypf1  25373  plyaddlem1  25374  plymullem1  25375  plyaddlem  25376  plymullem  25377  plysub  25380  coeeulem  25385  coeeq  25388  dgrlem  25390  coeidlem  25398  plyco  25402  coe0  25417  coesub  25418  dgrmulc  25432  dgrsub  25433  dgrcolem1  25434  dgrcolem2  25435  plymul0or  25441  dvnply2  25447  plycpn  25449  plydivlem3  25455  plydivlem4  25456  plydiveu  25458  plyremlem  25464  plyrem  25465  facth  25466  fta1lem  25467  quotcan  25469  vieta1lem2  25471  plyexmo  25473  elqaalem3  25481  qaa  25483  iaa  25485  aannenlem1  25488  aannenlem2  25489  aannenlem3  25490  taylfvallem1  25516  taylfval  25518  tayl0  25521  taylplem1  25522  taylply2  25527  taylply  25528  dvtaylp  25529  dvntaylp  25530  dvntaylp0  25531  taylthlem1  25532  taylthlem2  25533  ulmval  25539  ulmss  25556  ulmcn  25558  mtest  25563  pserulm  25581  psercn  25585  pserdvlem2  25587  abelth  25600  reefgim  25609  cxpcn2  25899  logbmpt  25938  logbfval  25940  lgamgulmlem5  26182  lgamgulmlem6  26183  lgamgulm2  26185  lgamcvglem  26189  ftalem7  26228  dchrfi  26403  cffldtocusgr  27814  isvcOLD  28941  cnaddabloOLD  28943  cnnvg  29040  cnnvs  29042  cnnvnm  29043  cncph  29181  hvmulex  29373  hfsmval  30100  hfmmval  30101  nmfnval  30238  nlfnval  30243  elcnfn  30244  ellnfn  30245  specval  30260  hhcnf  30267  lmlim  31897  esumcvg  32054  plymul02  32525  plymulx0  32526  signsplypnf  32529  signsply0  32530  breprexplemb  32611  breprexpnat  32614  vtsval  32617  circlemethnat  32621  circlevma  32622  circlemethhgt  32623  cvxpconn  33204  fwddifval  34464  fwddifnval  34465  ivthALT  34524  knoppcnlem5  34677  knoppcnlem8  34680  bj-inftyexpiinv  35379  bj-inftyexpidisj  35381  caures  35918  cntotbnd  35954  cnpwstotbnd  35955  rrnval  35985  cnaddcom  36986  elmnc  40961  mpaaeu  40975  itgoval  40986  itgocn  40989  rngunsnply  40998  binomcxplemnotnn0  41974  climexp  43146  xlimbr  43368  fuzxrpmcn  43369  xlimmnfvlem2  43374  xlimpnfvlem2  43378  mulcncff  43411  subcncff  43421  addcncff  43425  cncfuni  43427  divcncff  43432  dvsinax  43454  dvcosax  43467  dvnmptdivc  43479  dvnmptconst  43482  dvnxpaek  43483  dvnmul  43484  dvnprodlem3  43489  etransclem1  43776  etransclem2  43777  etransclem4  43779  etransclem13  43788  etransclem46  43821  fdivpm  45889  amgmlemALT  46507
  Copyright terms: Public domain W3C validator