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

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

Proof of Theorem cnex
StepHypRef Expression
1 ax-cnex 11071 1 ℂ ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2113  Vcvv 3437  cc 11013
This theorem was proved from axioms:  ax-cnex 11071
This theorem is referenced by:  reex  11106  cnelprrecn  11108  pnfex  11174  nnex  12140  zex  12486  qex  12863  mpoaddex  12890  addex  12891  mpomulex  12892  mulex  12893  rlim  15406  rlimf  15412  rlimss  15413  elo12  15438  o1f  15440  o1dm  15441  cnso  16160  cnaddablx  19784  cnaddabl  19785  cnaddid  19786  cnaddinv  19787  cnfldbas  21299  cnfldcj  21304  cnfldds  21307  cnfldfun  21309  cnfldfunALT  21310  cnfldbasOLD  21314  cnfldcjOLD  21317  cnflddsOLD  21320  cnfldfunOLD  21322  cnfldfunALTOLD  21323  cnmsubglem  21371  cnmsgngrp  21520  psgninv  21523  lmbrf  23178  lmfss  23214  lmres  23218  lmcnp  23222  cnmet  24689  cncfval  24811  elcncf  24812  cncfcnvcn  24849  cnheibor  24884  cnlmodlem1  25066  tcphex  25147  tchnmfval  25158  tcphcph  25167  lmmbr2  25189  lmmbrf  25192  iscau2  25207  iscauf  25210  caucfil  25213  cmetcaulem  25218  caussi  25227  causs  25228  lmclimf  25234  mbff  25556  ismbf  25559  ismbfcn  25560  mbfconst  25564  mbfres  25575  mbfimaopn2  25588  cncombf  25589  cnmbf  25590  0plef  25603  0pledm  25604  itg1ge0  25617  mbfi1fseqlem5  25650  itg2addlem  25689  limcfval  25803  limcrcl  25805  ellimc2  25808  limcflf  25812  limcres  25817  limcun  25826  dvfval  25828  dvbss  25832  dvbsss  25833  perfdvf  25834  dvreslem  25840  dvres2lem  25841  dvcnp2  25851  dvcnp2OLD  25852  dvnfval  25854  dvnff  25855  dvnf  25859  dvnbss  25860  dvnadd  25861  dvn2bss  25862  dvnres  25863  cpnfval  25864  cpnord  25867  dvaddbr  25870  dvmulbr  25871  dvmulbrOLD  25872  dvnfre  25886  dvexp  25887  dvef  25914  c1liplem1  25931  c1lip2  25933  lhop1lem  25948  plyval  26128  elply  26130  elply2  26131  plyf  26133  plyss  26134  elplyr  26136  plyeq0lem  26145  plyeq0  26146  plypf1  26147  plyaddlem1  26148  plymullem1  26149  plyaddlem  26150  plymullem  26151  plysub  26154  coeeulem  26159  coeeq  26162  dgrlem  26164  coeidlem  26172  plyco  26176  coe0  26191  coesub  26192  dgrmulc  26207  dgrsub  26208  dgrcolem1  26209  dgrcolem2  26210  plymul0or  26218  dvnply2  26225  plycpn  26227  plydivlem3  26233  plydivlem4  26234  plydiveu  26236  plyremlem  26242  plyrem  26243  facth  26244  fta1lem  26245  quotcan  26247  vieta1lem2  26249  plyexmo  26251  elqaalem3  26259  qaa  26261  iaa  26263  aannenlem1  26266  aannenlem2  26267  aannenlem3  26268  taylfvallem1  26294  taylfval  26296  tayl0  26299  taylplem1  26300  taylply2  26305  taylply2OLD  26306  taylply  26307  dvtaylp  26308  dvntaylp  26309  dvntaylp0  26310  taylthlem1  26311  taylthlem2  26312  taylthlem2OLD  26313  ulmval  26319  ulmss  26336  ulmcn  26338  mtest  26343  pserulm  26361  psercn  26366  pserdvlem2  26368  abelth  26381  reefgim  26390  cxpcn2  26686  logbmpt  26728  logbfval  26730  lgamgulmlem5  26973  lgamgulmlem6  26974  lgamgulm2  26976  lgamcvglem  26980  ftalem7  27019  dchrfi  27196  cffldtocusgr  29429  cffldtocusgrOLD  29430  isvcOLD  30563  cnaddabloOLD  30565  cnnvg  30662  cnnvs  30664  cnnvnm  30665  cncph  30803  hvmulex  30995  hfsmval  31722  hfmmval  31723  nmfnval  31860  nlfnval  31865  elcnfn  31866  ellnfn  31867  specval  31882  hhcnf  31889  constrsuc  33774  lmlim  33983  esumcvg  34122  plymul02  34582  plymulx0  34583  signsplypnf  34586  signsply0  34587  breprexplemb  34667  breprexpnat  34670  vtsval  34673  circlemethnat  34677  circlevma  34678  circlemethhgt  34679  cvxpconn  35309  fwddifval  36229  fwddifnval  36230  ivthALT  36402  knoppcnlem5  36564  knoppcnlem8  36567  bj-inftyexpiinv  37275  bj-inftyexpidisj  37277  caures  37823  cntotbnd  37859  cnpwstotbnd  37860  rrnval  37890  cnaddcom  39094  subex  42368  absex  42369  cjex  42370  elmnc  43256  mpaaeu  43270  itgoval  43281  itgocn  43284  rngunsnply  43289  binomcxplemnotnn0  44476  climexp  45732  xlimbr  45952  fuzxrpmcn  45953  xlimmnfvlem2  45958  xlimpnfvlem2  45962  mulcncff  45995  subcncff  46005  addcncff  46009  cncfuni  46011  divcncff  46016  dvsinax  46038  dvcosax  46051  dvnmptdivc  46063  dvnmptconst  46066  dvnxpaek  46067  dvnmul  46068  dvnprodlem3  46073  etransclem1  46360  etransclem2  46361  etransclem4  46363  etransclem13  46372  etransclem46  46405  nthrucw  47011  cjnpoly  47016  fdivpm  48671  amgmlemALT  49931
  Copyright terms: Public domain W3C validator