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

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

Proof of Theorem cnex
StepHypRef Expression
1 ax-cnex 11185 1 ℂ ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2108  Vcvv 3459  cc 11127
This theorem was proved from axioms:  ax-cnex 11185
This theorem is referenced by:  reex  11220  cnelprrecn  11222  pnfex  11288  nnex  12246  zex  12597  qex  12977  mpoaddex  13004  addex  13005  mpomulex  13006  mulex  13007  rlim  15511  rlimf  15517  rlimss  15518  elo12  15543  o1f  15545  o1dm  15546  cnso  16265  cnaddablx  19849  cnaddabl  19850  cnaddid  19851  cnaddinv  19852  cnfldbas  21319  cnfldcj  21324  cnfldds  21327  cnfldfun  21329  cnfldfunALT  21330  cnfldbasOLD  21334  cnfldcjOLD  21337  cnflddsOLD  21340  cnfldfunOLD  21342  cnfldfunALTOLD  21343  cnmsubglem  21398  cnmsgngrp  21539  psgninv  21542  lmbrf  23198  lmfss  23234  lmres  23238  lmcnp  23242  cnmet  24710  cncfval  24832  elcncf  24833  cncfcnvcn  24870  cnheibor  24905  cnlmodlem1  25087  tcphex  25169  tchnmfval  25180  tcphcph  25189  lmmbr2  25211  lmmbrf  25214  iscau2  25229  iscauf  25232  caucfil  25235  cmetcaulem  25240  caussi  25249  causs  25250  lmclimf  25256  mbff  25578  ismbf  25581  ismbfcn  25582  mbfconst  25586  mbfres  25597  mbfimaopn2  25610  cncombf  25611  cnmbf  25612  0plef  25625  0pledm  25626  itg1ge0  25639  mbfi1fseqlem5  25672  itg2addlem  25711  limcfval  25825  limcrcl  25827  ellimc2  25830  limcflf  25834  limcres  25839  limcun  25848  dvfval  25850  dvbss  25854  dvbsss  25855  perfdvf  25856  dvreslem  25862  dvres2lem  25863  dvcnp2  25873  dvcnp2OLD  25874  dvnfval  25876  dvnff  25877  dvnf  25881  dvnbss  25882  dvnadd  25883  dvn2bss  25884  dvnres  25885  cpnfval  25886  cpnord  25889  dvaddbr  25892  dvmulbr  25893  dvmulbrOLD  25894  dvnfre  25908  dvexp  25909  dvef  25936  c1liplem1  25953  c1lip2  25955  lhop1lem  25970  plyval  26150  elply  26152  elply2  26153  plyf  26155  plyss  26156  elplyr  26158  plyeq0lem  26167  plyeq0  26168  plypf1  26169  plyaddlem1  26170  plymullem1  26171  plyaddlem  26172  plymullem  26173  plysub  26176  coeeulem  26181  coeeq  26184  dgrlem  26186  coeidlem  26194  plyco  26198  coe0  26213  coesub  26214  dgrmulc  26229  dgrsub  26230  dgrcolem1  26231  dgrcolem2  26232  plymul0or  26240  dvnply2  26247  plycpn  26249  plydivlem3  26255  plydivlem4  26256  plydiveu  26258  plyremlem  26264  plyrem  26265  facth  26266  fta1lem  26267  quotcan  26269  vieta1lem2  26271  plyexmo  26273  elqaalem3  26281  qaa  26283  iaa  26285  aannenlem1  26288  aannenlem2  26289  aannenlem3  26290  taylfvallem1  26316  taylfval  26318  tayl0  26321  taylplem1  26322  taylply2  26327  taylply2OLD  26328  taylply  26329  dvtaylp  26330  dvntaylp  26331  dvntaylp0  26332  taylthlem1  26333  taylthlem2  26334  taylthlem2OLD  26335  ulmval  26341  ulmss  26358  ulmcn  26360  mtest  26365  pserulm  26383  psercn  26388  pserdvlem2  26390  abelth  26403  reefgim  26412  cxpcn2  26708  logbmpt  26750  logbfval  26752  lgamgulmlem5  26995  lgamgulmlem6  26996  lgamgulm2  26998  lgamcvglem  27002  ftalem7  27041  dchrfi  27218  cffldtocusgr  29426  cffldtocusgrOLD  29427  isvcOLD  30560  cnaddabloOLD  30562  cnnvg  30659  cnnvs  30661  cnnvnm  30662  cncph  30800  hvmulex  30992  hfsmval  31719  hfmmval  31720  nmfnval  31857  nlfnval  31862  elcnfn  31863  ellnfn  31864  specval  31879  hhcnf  31886  constrsuc  33772  lmlim  33978  esumcvg  34117  plymul02  34578  plymulx0  34579  signsplypnf  34582  signsply0  34583  breprexplemb  34663  breprexpnat  34666  vtsval  34669  circlemethnat  34673  circlevma  34674  circlemethhgt  34675  cvxpconn  35264  fwddifval  36180  fwddifnval  36181  ivthALT  36353  knoppcnlem5  36515  knoppcnlem8  36518  bj-inftyexpiinv  37226  bj-inftyexpidisj  37228  caures  37784  cntotbnd  37820  cnpwstotbnd  37821  rrnval  37851  cnaddcom  38990  subex  42298  absex  42299  cjex  42300  elmnc  43160  mpaaeu  43174  itgoval  43185  itgocn  43188  rngunsnply  43193  binomcxplemnotnn0  44380  climexp  45634  xlimbr  45856  fuzxrpmcn  45857  xlimmnfvlem2  45862  xlimpnfvlem2  45866  mulcncff  45899  subcncff  45909  addcncff  45913  cncfuni  45915  divcncff  45920  dvsinax  45942  dvcosax  45955  dvnmptdivc  45967  dvnmptconst  45970  dvnxpaek  45971  dvnmul  45972  dvnprodlem3  45977  etransclem1  46264  etransclem2  46265  etransclem4  46267  etransclem13  46276  etransclem46  46309  fdivpm  48523  amgmlemALT  49667
  Copyright terms: Public domain W3C validator