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

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

Proof of Theorem cnex
StepHypRef Expression
1 ax-cnex 11032 1 ℂ ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2106  Vcvv 3442  cc 10974
This theorem was proved from axioms:  ax-cnex 11032
This theorem is referenced by:  reex  11067  cnelprrecn  11069  pnfex  11133  nnex  12084  zex  12433  qex  12806  addex  12833  mulex  12834  rlim  15303  rlimf  15309  rlimss  15310  elo12  15335  o1f  15337  o1dm  15338  cnso  16055  cnaddablx  19564  cnaddabl  19565  cnaddid  19566  cnaddinv  19567  cnfldbas  20706  cnfldcj  20709  cnfldds  20712  cnfldfun  20714  cnfldfunALT  20715  cnfldfunALTOLD  20716  cnmsubglem  20766  cnmsgngrp  20889  psgninv  20892  lmbrf  22516  lmfss  22552  lmres  22556  lmcnp  22560  cnmet  24040  cncfval  24156  elcncf  24157  cncfcnvcn  24193  cnheibor  24223  cnlmodlem1  24404  tcphex  24486  tchnmfval  24497  tcphcph  24506  lmmbr2  24528  lmmbrf  24531  iscau2  24546  iscauf  24549  caucfil  24552  cmetcaulem  24557  caussi  24566  causs  24567  lmclimf  24573  mbff  24894  ismbf  24897  ismbfcn  24898  mbfconst  24902  mbfres  24913  mbfimaopn2  24926  cncombf  24927  cnmbf  24928  0plef  24941  0pledm  24942  itg1ge0  24955  mbfi1fseqlem5  24989  itg2addlem  25028  limcfval  25141  limcrcl  25143  ellimc2  25146  limcflf  25150  limcres  25155  limcun  25164  dvfval  25166  dvbss  25170  dvbsss  25171  perfdvf  25172  dvreslem  25178  dvres2lem  25179  dvcnp2  25189  dvnfval  25191  dvnff  25192  dvnf  25196  dvnbss  25197  dvnadd  25198  dvn2bss  25199  dvnres  25200  cpnfval  25201  cpnord  25204  dvaddbr  25207  dvmulbr  25208  dvnfre  25221  dvexp  25222  dvef  25249  c1liplem1  25265  c1lip2  25267  lhop1lem  25282  plyval  25459  elply  25461  elply2  25462  plyf  25464  plyss  25465  elplyr  25467  plyeq0lem  25476  plyeq0  25477  plypf1  25478  plyaddlem1  25479  plymullem1  25480  plyaddlem  25481  plymullem  25482  plysub  25485  coeeulem  25490  coeeq  25493  dgrlem  25495  coeidlem  25503  plyco  25507  coe0  25522  coesub  25523  dgrmulc  25537  dgrsub  25538  dgrcolem1  25539  dgrcolem2  25540  plymul0or  25546  dvnply2  25552  plycpn  25554  plydivlem3  25560  plydivlem4  25561  plydiveu  25563  plyremlem  25569  plyrem  25570  facth  25571  fta1lem  25572  quotcan  25574  vieta1lem2  25576  plyexmo  25578  elqaalem3  25586  qaa  25588  iaa  25590  aannenlem1  25593  aannenlem2  25594  aannenlem3  25595  taylfvallem1  25621  taylfval  25623  tayl0  25626  taylplem1  25627  taylply2  25632  taylply  25633  dvtaylp  25634  dvntaylp  25635  dvntaylp0  25636  taylthlem1  25637  taylthlem2  25638  ulmval  25644  ulmss  25661  ulmcn  25663  mtest  25668  pserulm  25686  psercn  25690  pserdvlem2  25692  abelth  25705  reefgim  25714  cxpcn2  26004  logbmpt  26043  logbfval  26045  lgamgulmlem5  26287  lgamgulmlem6  26288  lgamgulm2  26290  lgamcvglem  26294  ftalem7  26333  dchrfi  26508  cffldtocusgr  28102  isvcOLD  29228  cnaddabloOLD  29230  cnnvg  29327  cnnvs  29329  cnnvnm  29330  cncph  29468  hvmulex  29660  hfsmval  30387  hfmmval  30388  nmfnval  30525  nlfnval  30530  elcnfn  30531  ellnfn  30532  specval  30547  hhcnf  30554  lmlim  32193  esumcvg  32350  plymul02  32823  plymulx0  32824  signsplypnf  32827  signsply0  32828  breprexplemb  32909  breprexpnat  32912  vtsval  32915  circlemethnat  32919  circlevma  32920  circlemethhgt  32921  cvxpconn  33501  fwddifval  34601  fwddifnval  34602  ivthALT  34661  knoppcnlem5  34814  knoppcnlem8  34817  bj-inftyexpiinv  35533  bj-inftyexpidisj  35535  caures  36074  cntotbnd  36110  cnpwstotbnd  36111  rrnval  36141  cnaddcom  37290  elmnc  41275  mpaaeu  41289  itgoval  41300  itgocn  41303  rngunsnply  41312  binomcxplemnotnn0  42347  climexp  43534  xlimbr  43756  fuzxrpmcn  43757  xlimmnfvlem2  43762  xlimpnfvlem2  43766  mulcncff  43799  subcncff  43809  addcncff  43813  cncfuni  43815  divcncff  43820  dvsinax  43842  dvcosax  43855  dvnmptdivc  43867  dvnmptconst  43870  dvnxpaek  43871  dvnmul  43872  dvnprodlem3  43877  etransclem1  44164  etransclem2  44165  etransclem4  44167  etransclem13  44176  etransclem46  44209  fdivpm  46307  amgmlemALT  46925
  Copyright terms: Public domain W3C validator