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

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

Proof of Theorem cnex
StepHypRef Expression
1 ax-cnex 11082 1 ℂ ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2113  Vcvv 3440  cc 11024
This theorem was proved from axioms:  ax-cnex 11082
This theorem is referenced by:  reex  11117  cnelprrecn  11119  pnfex  11185  nnex  12151  zex  12497  qex  12874  mpoaddex  12901  addex  12902  mpomulex  12903  mulex  12904  rlim  15418  rlimf  15424  rlimss  15425  elo12  15450  o1f  15452  o1dm  15453  cnso  16172  cnaddablx  19797  cnaddabl  19798  cnaddid  19799  cnaddinv  19800  cnfldbas  21313  cnfldcj  21318  cnfldds  21321  cnfldfun  21323  cnfldfunALT  21324  cnfldbasOLD  21328  cnfldcjOLD  21331  cnflddsOLD  21334  cnfldfunOLD  21336  cnfldfunALTOLD  21337  cnmsubglem  21385  cnmsgngrp  21534  psgninv  21537  lmbrf  23204  lmfss  23240  lmres  23244  lmcnp  23248  cnmet  24715  cncfval  24837  elcncf  24838  cncfcnvcn  24875  cnheibor  24910  cnlmodlem1  25092  tcphex  25173  tchnmfval  25184  tcphcph  25193  lmmbr2  25215  lmmbrf  25218  iscau2  25233  iscauf  25236  caucfil  25239  cmetcaulem  25244  caussi  25253  causs  25254  lmclimf  25260  mbff  25582  ismbf  25585  ismbfcn  25586  mbfconst  25590  mbfres  25601  mbfimaopn2  25614  cncombf  25615  cnmbf  25616  0plef  25629  0pledm  25630  itg1ge0  25643  mbfi1fseqlem5  25676  itg2addlem  25715  limcfval  25829  limcrcl  25831  ellimc2  25834  limcflf  25838  limcres  25843  limcun  25852  dvfval  25854  dvbss  25858  dvbsss  25859  perfdvf  25860  dvreslem  25866  dvres2lem  25867  dvcnp2  25877  dvcnp2OLD  25878  dvnfval  25880  dvnff  25881  dvnf  25885  dvnbss  25886  dvnadd  25887  dvn2bss  25888  dvnres  25889  cpnfval  25890  cpnord  25893  dvaddbr  25896  dvmulbr  25897  dvmulbrOLD  25898  dvnfre  25912  dvexp  25913  dvef  25940  c1liplem1  25957  c1lip2  25959  lhop1lem  25974  plyval  26154  elply  26156  elply2  26157  plyf  26159  plyss  26160  elplyr  26162  plyeq0lem  26171  plyeq0  26172  plypf1  26173  plyaddlem1  26174  plymullem1  26175  plyaddlem  26176  plymullem  26177  plysub  26180  coeeulem  26185  coeeq  26188  dgrlem  26190  coeidlem  26198  plyco  26202  coe0  26217  coesub  26218  dgrmulc  26233  dgrsub  26234  dgrcolem1  26235  dgrcolem2  26236  plymul0or  26244  dvnply2  26251  plycpn  26253  plydivlem3  26259  plydivlem4  26260  plydiveu  26262  plyremlem  26268  plyrem  26269  facth  26270  fta1lem  26271  quotcan  26273  vieta1lem2  26275  plyexmo  26277  elqaalem3  26285  qaa  26287  iaa  26289  aannenlem1  26292  aannenlem2  26293  aannenlem3  26294  taylfvallem1  26320  taylfval  26322  tayl0  26325  taylplem1  26326  taylply2  26331  taylply2OLD  26332  taylply  26333  dvtaylp  26334  dvntaylp  26335  dvntaylp0  26336  taylthlem1  26337  taylthlem2  26338  taylthlem2OLD  26339  ulmval  26345  ulmss  26362  ulmcn  26364  mtest  26369  pserulm  26387  psercn  26392  pserdvlem2  26394  abelth  26407  reefgim  26416  cxpcn2  26712  logbmpt  26754  logbfval  26756  lgamgulmlem5  26999  lgamgulmlem6  27000  lgamgulm2  27002  lgamcvglem  27006  ftalem7  27045  dchrfi  27222  cffldtocusgr  29520  cffldtocusgrOLD  29521  isvcOLD  30654  cnaddabloOLD  30656  cnnvg  30753  cnnvs  30755  cnnvnm  30756  cncph  30894  hvmulex  31086  hfsmval  31813  hfmmval  31814  nmfnval  31951  nlfnval  31956  elcnfn  31957  ellnfn  31958  specval  31973  hhcnf  31980  constrsuc  33895  lmlim  34104  esumcvg  34243  plymul02  34703  plymulx0  34704  signsplypnf  34707  signsply0  34708  breprexplemb  34788  breprexpnat  34791  vtsval  34794  circlemethnat  34798  circlevma  34799  circlemethhgt  34800  cvxpconn  35436  fwddifval  36356  fwddifnval  36357  ivthALT  36529  knoppcnlem5  36697  knoppcnlem8  36700  bj-inftyexpiinv  37413  bj-inftyexpidisj  37415  caures  37961  cntotbnd  37997  cnpwstotbnd  37998  rrnval  38028  cnaddcom  39232  subex  42502  absex  42503  cjex  42504  elmnc  43378  mpaaeu  43392  itgoval  43403  itgocn  43406  rngunsnply  43411  binomcxplemnotnn0  44597  climexp  45851  xlimbr  46071  fuzxrpmcn  46072  xlimmnfvlem2  46077  xlimpnfvlem2  46081  mulcncff  46114  subcncff  46124  addcncff  46128  cncfuni  46130  divcncff  46135  dvsinax  46157  dvcosax  46170  dvnmptdivc  46182  dvnmptconst  46185  dvnxpaek  46186  dvnmul  46187  dvnprodlem3  46192  etransclem1  46479  etransclem2  46480  etransclem4  46482  etransclem13  46491  etransclem46  46524  nthrucw  47130  cjnpoly  47135  fdivpm  48789  amgmlemALT  50048
  Copyright terms: Public domain W3C validator