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

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

Proof of Theorem cnex
StepHypRef Expression
1 ax-cnex 11094 1 ℂ ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2114  Vcvv 3442  cc 11036
This theorem was proved from axioms:  ax-cnex 11094
This theorem is referenced by:  reex  11129  cnelprrecn  11131  pnfex  11197  nnex  12163  zex  12509  qex  12886  mpoaddex  12913  addex  12914  mpomulex  12915  mulex  12916  rlim  15430  rlimf  15436  rlimss  15437  elo12  15462  o1f  15464  o1dm  15465  cnso  16184  cnaddablx  19809  cnaddabl  19810  cnaddid  19811  cnaddinv  19812  cnfldbas  21325  cnfldcj  21330  cnfldds  21333  cnfldfun  21335  cnfldfunALT  21336  cnfldbasOLD  21340  cnfldcjOLD  21343  cnflddsOLD  21346  cnfldfunOLD  21348  cnfldfunALTOLD  21349  cnmsubglem  21397  cnmsgngrp  21546  psgninv  21549  lmbrf  23216  lmfss  23252  lmres  23256  lmcnp  23260  cnmet  24727  cncfval  24849  elcncf  24850  cncfcnvcn  24887  cnheibor  24922  cnlmodlem1  25104  tcphex  25185  tchnmfval  25196  tcphcph  25205  lmmbr2  25227  lmmbrf  25230  iscau2  25245  iscauf  25248  caucfil  25251  cmetcaulem  25256  caussi  25265  causs  25266  lmclimf  25272  mbff  25594  ismbf  25597  ismbfcn  25598  mbfconst  25602  mbfres  25613  mbfimaopn2  25626  cncombf  25627  cnmbf  25628  0plef  25641  0pledm  25642  itg1ge0  25655  mbfi1fseqlem5  25688  itg2addlem  25727  limcfval  25841  limcrcl  25843  ellimc2  25846  limcflf  25850  limcres  25855  limcun  25864  dvfval  25866  dvbss  25870  dvbsss  25871  perfdvf  25872  dvreslem  25878  dvres2lem  25879  dvcnp2  25889  dvcnp2OLD  25890  dvnfval  25892  dvnff  25893  dvnf  25897  dvnbss  25898  dvnadd  25899  dvn2bss  25900  dvnres  25901  cpnfval  25902  cpnord  25905  dvaddbr  25908  dvmulbr  25909  dvmulbrOLD  25910  dvnfre  25924  dvexp  25925  dvef  25952  c1liplem1  25969  c1lip2  25971  lhop1lem  25986  plyval  26166  elply  26168  elply2  26169  plyf  26171  plyss  26172  elplyr  26174  plyeq0lem  26183  plyeq0  26184  plypf1  26185  plyaddlem1  26186  plymullem1  26187  plyaddlem  26188  plymullem  26189  plysub  26192  coeeulem  26197  coeeq  26200  dgrlem  26202  coeidlem  26210  plyco  26214  coe0  26229  coesub  26230  dgrmulc  26245  dgrsub  26246  dgrcolem1  26247  dgrcolem2  26248  plymul0or  26256  dvnply2  26263  plycpn  26265  plydivlem3  26271  plydivlem4  26272  plydiveu  26274  plyremlem  26280  plyrem  26281  facth  26282  fta1lem  26283  quotcan  26285  vieta1lem2  26287  plyexmo  26289  elqaalem3  26297  qaa  26299  iaa  26301  aannenlem1  26304  aannenlem2  26305  aannenlem3  26306  taylfvallem1  26332  taylfval  26334  tayl0  26337  taylplem1  26338  taylply2  26343  taylply2OLD  26344  taylply  26345  dvtaylp  26346  dvntaylp  26347  dvntaylp0  26348  taylthlem1  26349  taylthlem2  26350  taylthlem2OLD  26351  ulmval  26357  ulmss  26374  ulmcn  26376  mtest  26381  pserulm  26399  psercn  26404  pserdvlem2  26406  abelth  26419  reefgim  26428  cxpcn2  26724  logbmpt  26766  logbfval  26768  lgamgulmlem5  27011  lgamgulmlem6  27012  lgamgulm2  27014  lgamcvglem  27018  ftalem7  27057  dchrfi  27234  cffldtocusgr  29532  cffldtocusgrOLD  29533  isvcOLD  30666  cnaddabloOLD  30668  cnnvg  30765  cnnvs  30767  cnnvnm  30768  cncph  30906  hvmulex  31098  hfsmval  31825  hfmmval  31826  nmfnval  31963  nlfnval  31968  elcnfn  31969  ellnfn  31970  specval  31985  hhcnf  31992  constrsuc  33915  lmlim  34124  esumcvg  34263  plymul02  34723  plymulx0  34724  signsplypnf  34727  signsply0  34728  breprexplemb  34808  breprexpnat  34811  vtsval  34814  circlemethnat  34818  circlevma  34819  circlemethhgt  34820  cvxpconn  35455  fwddifval  36375  fwddifnval  36376  ivthALT  36548  knoppcnlem5  36716  knoppcnlem8  36719  bj-inftyexpiinv  37460  bj-inftyexpidisj  37462  caures  38008  cntotbnd  38044  cnpwstotbnd  38045  rrnval  38075  cnaddcom  39345  subex  42614  absex  42615  cjex  42616  elmnc  43490  mpaaeu  43504  itgoval  43515  itgocn  43518  rngunsnply  43523  binomcxplemnotnn0  44709  climexp  45962  xlimbr  46182  fuzxrpmcn  46183  xlimmnfvlem2  46188  xlimpnfvlem2  46192  mulcncff  46225  subcncff  46235  addcncff  46239  cncfuni  46241  divcncff  46246  dvsinax  46268  dvcosax  46281  dvnmptdivc  46293  dvnmptconst  46296  dvnxpaek  46297  dvnmul  46298  dvnprodlem3  46303  etransclem1  46590  etransclem2  46591  etransclem4  46593  etransclem13  46602  etransclem46  46635  nthrucw  47241  cjnpoly  47246  fdivpm  48900  amgmlemALT  50159
  Copyright terms: Public domain W3C validator