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

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

Proof of Theorem cnex
StepHypRef Expression
1 ax-cnex 11072 1 ℂ ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2113  Vcvv 3438  cc 11014
This theorem was proved from axioms:  ax-cnex 11072
This theorem is referenced by:  reex  11107  cnelprrecn  11109  pnfex  11175  nnex  12141  zex  12487  qex  12869  mpoaddex  12896  addex  12897  mpomulex  12898  mulex  12899  rlim  15412  rlimf  15418  rlimss  15419  elo12  15444  o1f  15446  o1dm  15447  cnso  16166  cnaddablx  19790  cnaddabl  19791  cnaddid  19792  cnaddinv  19793  cnfldbas  21305  cnfldcj  21310  cnfldds  21313  cnfldfun  21315  cnfldfunALT  21316  cnfldbasOLD  21320  cnfldcjOLD  21323  cnflddsOLD  21326  cnfldfunOLD  21328  cnfldfunALTOLD  21329  cnmsubglem  21377  cnmsgngrp  21526  psgninv  21529  lmbrf  23185  lmfss  23221  lmres  23225  lmcnp  23229  cnmet  24696  cncfval  24818  elcncf  24819  cncfcnvcn  24856  cnheibor  24891  cnlmodlem1  25073  tcphex  25154  tchnmfval  25165  tcphcph  25174  lmmbr2  25196  lmmbrf  25199  iscau2  25214  iscauf  25217  caucfil  25220  cmetcaulem  25225  caussi  25234  causs  25235  lmclimf  25241  mbff  25563  ismbf  25566  ismbfcn  25567  mbfconst  25571  mbfres  25582  mbfimaopn2  25595  cncombf  25596  cnmbf  25597  0plef  25610  0pledm  25611  itg1ge0  25624  mbfi1fseqlem5  25657  itg2addlem  25696  limcfval  25810  limcrcl  25812  ellimc2  25815  limcflf  25819  limcres  25824  limcun  25833  dvfval  25835  dvbss  25839  dvbsss  25840  perfdvf  25841  dvreslem  25847  dvres2lem  25848  dvcnp2  25858  dvcnp2OLD  25859  dvnfval  25861  dvnff  25862  dvnf  25866  dvnbss  25867  dvnadd  25868  dvn2bss  25869  dvnres  25870  cpnfval  25871  cpnord  25874  dvaddbr  25877  dvmulbr  25878  dvmulbrOLD  25879  dvnfre  25893  dvexp  25894  dvef  25921  c1liplem1  25938  c1lip2  25940  lhop1lem  25955  plyval  26135  elply  26137  elply2  26138  plyf  26140  plyss  26141  elplyr  26143  plyeq0lem  26152  plyeq0  26153  plypf1  26154  plyaddlem1  26155  plymullem1  26156  plyaddlem  26157  plymullem  26158  plysub  26161  coeeulem  26166  coeeq  26169  dgrlem  26171  coeidlem  26179  plyco  26183  coe0  26198  coesub  26199  dgrmulc  26214  dgrsub  26215  dgrcolem1  26216  dgrcolem2  26217  plymul0or  26225  dvnply2  26232  plycpn  26234  plydivlem3  26240  plydivlem4  26241  plydiveu  26243  plyremlem  26249  plyrem  26250  facth  26251  fta1lem  26252  quotcan  26254  vieta1lem2  26256  plyexmo  26258  elqaalem3  26266  qaa  26268  iaa  26270  aannenlem1  26273  aannenlem2  26274  aannenlem3  26275  taylfvallem1  26301  taylfval  26303  tayl0  26306  taylplem1  26307  taylply2  26312  taylply2OLD  26313  taylply  26314  dvtaylp  26315  dvntaylp  26316  dvntaylp0  26317  taylthlem1  26318  taylthlem2  26319  taylthlem2OLD  26320  ulmval  26326  ulmss  26343  ulmcn  26345  mtest  26350  pserulm  26368  psercn  26373  pserdvlem2  26375  abelth  26388  reefgim  26397  cxpcn2  26693  logbmpt  26735  logbfval  26737  lgamgulmlem5  26980  lgamgulmlem6  26981  lgamgulm2  26983  lgamcvglem  26987  ftalem7  27026  dchrfi  27203  cffldtocusgr  29436  cffldtocusgrOLD  29437  isvcOLD  30570  cnaddabloOLD  30572  cnnvg  30669  cnnvs  30671  cnnvnm  30672  cncph  30810  hvmulex  31002  hfsmval  31729  hfmmval  31730  nmfnval  31867  nlfnval  31872  elcnfn  31873  ellnfn  31874  specval  31889  hhcnf  31896  constrsuc  33762  lmlim  33971  esumcvg  34110  plymul02  34570  plymulx0  34571  signsplypnf  34574  signsply0  34575  breprexplemb  34655  breprexpnat  34658  vtsval  34661  circlemethnat  34665  circlevma  34666  circlemethhgt  34667  cvxpconn  35297  fwddifval  36217  fwddifnval  36218  ivthALT  36390  knoppcnlem5  36552  knoppcnlem8  36555  bj-inftyexpiinv  37263  bj-inftyexpidisj  37265  caures  37810  cntotbnd  37846  cnpwstotbnd  37847  rrnval  37877  cnaddcom  39081  subex  42355  absex  42356  cjex  42357  elmnc  43243  mpaaeu  43257  itgoval  43268  itgocn  43271  rngunsnply  43276  binomcxplemnotnn0  44463  climexp  45719  xlimbr  45939  fuzxrpmcn  45940  xlimmnfvlem2  45945  xlimpnfvlem2  45949  mulcncff  45982  subcncff  45992  addcncff  45996  cncfuni  45998  divcncff  46003  dvsinax  46025  dvcosax  46038  dvnmptdivc  46050  dvnmptconst  46053  dvnxpaek  46054  dvnmul  46055  dvnprodlem3  46060  etransclem1  46347  etransclem2  46348  etransclem4  46350  etransclem13  46359  etransclem46  46392  nthrucw  46998  cjnpoly  47003  fdivpm  48658  amgmlemALT  49918
  Copyright terms: Public domain W3C validator