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

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

Proof of Theorem cnex
StepHypRef Expression
1 ax-cnex 11062 1 ℂ ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2111  Vcvv 3436  cc 11004
This theorem was proved from axioms:  ax-cnex 11062
This theorem is referenced by:  reex  11097  cnelprrecn  11099  pnfex  11165  nnex  12131  zex  12477  qex  12859  mpoaddex  12886  addex  12887  mpomulex  12888  mulex  12889  rlim  15402  rlimf  15408  rlimss  15409  elo12  15434  o1f  15436  o1dm  15437  cnso  16156  cnaddablx  19781  cnaddabl  19782  cnaddid  19783  cnaddinv  19784  cnfldbas  21296  cnfldcj  21301  cnfldds  21304  cnfldfun  21306  cnfldfunALT  21307  cnfldbasOLD  21311  cnfldcjOLD  21314  cnflddsOLD  21317  cnfldfunOLD  21319  cnfldfunALTOLD  21320  cnmsubglem  21368  cnmsgngrp  21517  psgninv  21520  lmbrf  23176  lmfss  23212  lmres  23216  lmcnp  23220  cnmet  24687  cncfval  24809  elcncf  24810  cncfcnvcn  24847  cnheibor  24882  cnlmodlem1  25064  tcphex  25145  tchnmfval  25156  tcphcph  25165  lmmbr2  25187  lmmbrf  25190  iscau2  25205  iscauf  25208  caucfil  25211  cmetcaulem  25216  caussi  25225  causs  25226  lmclimf  25232  mbff  25554  ismbf  25557  ismbfcn  25558  mbfconst  25562  mbfres  25573  mbfimaopn2  25586  cncombf  25587  cnmbf  25588  0plef  25601  0pledm  25602  itg1ge0  25615  mbfi1fseqlem5  25648  itg2addlem  25687  limcfval  25801  limcrcl  25803  ellimc2  25806  limcflf  25810  limcres  25815  limcun  25824  dvfval  25826  dvbss  25830  dvbsss  25831  perfdvf  25832  dvreslem  25838  dvres2lem  25839  dvcnp2  25849  dvcnp2OLD  25850  dvnfval  25852  dvnff  25853  dvnf  25857  dvnbss  25858  dvnadd  25859  dvn2bss  25860  dvnres  25861  cpnfval  25862  cpnord  25865  dvaddbr  25868  dvmulbr  25869  dvmulbrOLD  25870  dvnfre  25884  dvexp  25885  dvef  25912  c1liplem1  25929  c1lip2  25931  lhop1lem  25946  plyval  26126  elply  26128  elply2  26129  plyf  26131  plyss  26132  elplyr  26134  plyeq0lem  26143  plyeq0  26144  plypf1  26145  plyaddlem1  26146  plymullem1  26147  plyaddlem  26148  plymullem  26149  plysub  26152  coeeulem  26157  coeeq  26160  dgrlem  26162  coeidlem  26170  plyco  26174  coe0  26189  coesub  26190  dgrmulc  26205  dgrsub  26206  dgrcolem1  26207  dgrcolem2  26208  plymul0or  26216  dvnply2  26223  plycpn  26225  plydivlem3  26231  plydivlem4  26232  plydiveu  26234  plyremlem  26240  plyrem  26241  facth  26242  fta1lem  26243  quotcan  26245  vieta1lem2  26247  plyexmo  26249  elqaalem3  26257  qaa  26259  iaa  26261  aannenlem1  26264  aannenlem2  26265  aannenlem3  26266  taylfvallem1  26292  taylfval  26294  tayl0  26297  taylplem1  26298  taylply2  26303  taylply2OLD  26304  taylply  26305  dvtaylp  26306  dvntaylp  26307  dvntaylp0  26308  taylthlem1  26309  taylthlem2  26310  taylthlem2OLD  26311  ulmval  26317  ulmss  26334  ulmcn  26336  mtest  26341  pserulm  26359  psercn  26364  pserdvlem2  26366  abelth  26379  reefgim  26388  cxpcn2  26684  logbmpt  26726  logbfval  26728  lgamgulmlem5  26971  lgamgulmlem6  26972  lgamgulm2  26974  lgamcvglem  26978  ftalem7  27017  dchrfi  27194  cffldtocusgr  29426  cffldtocusgrOLD  29427  isvcOLD  30557  cnaddabloOLD  30559  cnnvg  30656  cnnvs  30658  cnnvnm  30659  cncph  30797  hvmulex  30989  hfsmval  31716  hfmmval  31717  nmfnval  31854  nlfnval  31859  elcnfn  31860  ellnfn  31861  specval  31876  hhcnf  31883  constrsuc  33749  lmlim  33958  esumcvg  34097  plymul02  34557  plymulx0  34558  signsplypnf  34561  signsply0  34562  breprexplemb  34642  breprexpnat  34645  vtsval  34648  circlemethnat  34652  circlevma  34653  circlemethhgt  34654  cvxpconn  35284  fwddifval  36202  fwddifnval  36203  ivthALT  36375  knoppcnlem5  36537  knoppcnlem8  36540  bj-inftyexpiinv  37248  bj-inftyexpidisj  37250  caures  37806  cntotbnd  37842  cnpwstotbnd  37843  rrnval  37873  cnaddcom  39017  subex  42286  absex  42287  cjex  42288  elmnc  43175  mpaaeu  43189  itgoval  43200  itgocn  43203  rngunsnply  43208  binomcxplemnotnn0  44395  climexp  45651  xlimbr  45871  fuzxrpmcn  45872  xlimmnfvlem2  45877  xlimpnfvlem2  45881  mulcncff  45914  subcncff  45924  addcncff  45928  cncfuni  45930  divcncff  45935  dvsinax  45957  dvcosax  45970  dvnmptdivc  45982  dvnmptconst  45985  dvnxpaek  45986  dvnmul  45987  dvnprodlem3  45992  etransclem1  46279  etransclem2  46280  etransclem4  46282  etransclem13  46291  etransclem46  46324  cjnpoly  46926  fdivpm  48581  amgmlemALT  49841
  Copyright terms: Public domain W3C validator