Theorem cnex 11274

Description: Alias for ax-cnex 11249. See also cnexALT 13107. (Contributed by Mario Carneiro, 17-Nov-2014.)

Assertion

Ref	Expression
cnex	⊢ ℂ ∈ V

Proof of Theorem cnex

Step	Hyp	Ref	Expression
1		ax-cnex 11249	1 ⊢ ℂ ∈ V

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3451  ℂcc 11191

This proof depends on axioms:  ax-cnex 11249

This theorem is used by:  reex  11284  cnelprrecn  11286  pnfex  11355  nnex  12334  zex  12695  qex  13081  mpoaddex  13109  addex  13110  mpomulex  13111  mulex  13112  rlim  15655  rlimf  15661  rlimss  15662  elo12  15687  o1f  15689  o1dm  15690  cnso  16408  cnaddablx  20075  cnaddabl  20076  cnaddid  20077  cnaddinv  20078  cnfldbas  21675  cnfldcj  21680  cnfldds  21683  cnfldfun  21685  cnfldfunALT  21686  cnmsubglem  21729  cnmsgngrp  21878  psgninv  21881  lmbrf  23571  lmfss  23607  lmres  23611  lmcnp  23615  cnmet  25083  cncfval  25202  elcncf  25203  cncfcnvcn  25239  cnheibor  25269  cnlmodlem1  25450  tcphex  25531  tchnmfval  25542  tcphcph  25551  lmmbr2  25573  lmmbrf  25576  iscau2  25591  iscauf  25594  caucfil  25597  cmetcaulem  25602  caussi  25611  causs  25612  lmclimf  25618  mbff  25939  ismbf  25942  ismbfcn  25943  mbfconst  25947  mbfres  25958  mbfimaopn2  25971  cncombf  25972  cnmbf  25973  0plef  25986  0pledm  25987  itg1ge0  26000  mbfi1fseqlem5  26033  itg2addlem  26072  limcfval  26185  limcrcl  26187  ellimc2  26190  limcflf  26194  limcres  26199  limcun  26208  dvfval  26210  dvbss  26214  dvbsss  26215  perfdvf  26216  dvreslem  26222  dvres2lem  26223  dvcnp2  26233  dvnfval  26235  dvnff  26236  dvnf  26240  dvnbss  26241  dvnadd  26242  dvn2bss  26243  dvnres  26244  cpnfval  26245  cpnord  26248  dvaddbr  26251  dvmulbr  26252  dvnfre  26265  dvexp  26266  dvef  26293  c1liplem1  26309  c1lip2  26311  lhop1lem  26326  plyval  26504  elply  26506  elply2  26507  plyf  26509  plyss  26510  elplyr  26512  plyeq0lem  26522  plyeq0  26523  plypf1  26524  plyaddlem1  26525  plymullem1  26526  plyaddlem  26527  plymullem  26528  plysub  26531  coeeulem  26536  coeeq  26539  dgrlem  26541  coeidlem  26549  plyco  26553  coe0  26568  coesub  26569  dgrmulc  26583  dgrsub  26584  dgrcolem1  26585  dgrcolem2  26586  plymul0or  26592  plymul02  26594  plyn0mulidp  26595  dvnply2  26601  plycpn  26603  plydivlem3  26609  plydivlem4  26610  plydiveu  26612  plyremlem  26618  plyrem  26619  facth  26620  fta1lem  26621  rnplynfin  26623  quotcan  26625  vieta1lem2  26627  plyexmo  26629  elqaalem3  26637  qaa  26640  iaaOLD  26645  aannenlem1  26648  aannenlem2  26649  aannenlem3  26650  taylfvallem1  26677  taylfval  26679  tayl0  26682  taylplem1  26683  taylply2  26688  taylply  26689  dvtaylp  26690  dvntaylp  26691  dvntaylp0  26692  taylthlem1  26693  taylthlem2  26694  ulmval  26700  ulmss  26717  ulmcn  26719  mtest  26724  pserulm  26742  psercn  26746  pserdvlem2  26748  abelth  26761  reefgim  26770  cxpcn2  27067  logbmpt  27109  logbfval  27111  lgamgulmlem5  27353  lgamgulmlem6  27354  lgamgulm2  27356  lgamcvglem  27360  ftalem7  27399  dchrfi  27575  cffldtocusgr  30021  isvcOLD  31174  cnaddabloOLD  31176  cnnvg  31273  cnnvs  31275  cnnvnm  31276  cncph  31414  hvmulex  31606  hfsmval  32333  hfmmval  32334  nmfnval  32471  nlfnval  32476  elcnfn  32477  ellnfn  32478  specval  32493  hhcnf  32500  constrsuc  34363  lmlim  34572  esumcvg  34711  signsplypnf  35172  signsply0  35173  breprexplemb  35253  breprexpnat  35256  vtsval  35259  circlemethnat  35263  circlevma  35264  circlemethhgt  35265  cvxpconn  35986  fwddifval  36907  fwddifnval  36908  ivthALT  37103  knoppcnlem5  37343  knoppcnlem8  37346  bj-inftyexpiinv  38109  bj-inftyexpidisj  38111  caures  38674  cntotbnd  38710  cnpwstotbnd  38711  rrnval  38741  cnaddcom  40009  subex  43278  absex  43279  cjex  43280  elmnc  44122  mpaaeu  44136  itgoval  44147  itgocn  44150  rngunsnply  44155  binomcxplemnotnn0  45325  climexp  46586  xlimbr  46806  fuzxrpmcn  46807  xlimmnfvlem2  46812  xlimpnfvlem2  46816  mulcncff  46849  subcncff  46859  addcncff  46863  cncfuni  46865  divcncff  46870  dvsinax  46892  dvcosax  46905  dvnmptdivc  46917  dvnmptconst  46920  dvnxpaek  46921  dvnmul  46922  dvnprodlem3  46927  etransclem1  47214  etransclem2  47215  etransclem4  47217  etransclem13  47226  etransclem46  47259  sqrtnnaa  47882  sqrtnzqaa  47883  numtowerdt  47885  cjnpoly  47908  fdivpm  49624  amgmlemALT  50957