Theorem cnex 11318

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

Assertion

Ref	Expression
cnex	⊢ ℂ ∈ V

Proof of Theorem cnex

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

This proof depends on syntax axioms:   ∈ wcel 2147  Vcvv 3454  ℂcc 11235

This proof depends on axioms:  ax-cnex 11293

This theorem is used by:  reex  11328  cnelprrecn  11330  pnfex  11399  nnex  12379  zex  12740  qex  13126  mpoaddex  13154  addex  13155  mpomulex  13156  mulex  13157  rlim  15703  rlimf  15709  rlimss  15710  elo12  15735  o1f  15737  o1dm  15738  cnso  16456  cnaddablx  20124  cnaddabl  20125  cnaddid  20126  cnaddinv  20127  cnfldbas  21724  cnfldcj  21729  cnfldds  21732  cnfldfun  21734  cnfldfunALT  21735  cnmsubglem  21780  cnmsgngrp  21929  psgninv  21932  lmbrf  23622  lmfss  23658  lmres  23662  lmcnp  23666  cnmet  25134  cncfval  25253  elcncf  25254  cncfcnvcn  25290  cnheibor  25320  cnlmodlem1  25501  tcphex  25582  tchnmfval  25593  tcphcph  25602  lmmbr2  25624  lmmbrf  25627  iscau2  25642  iscauf  25645  caucfil  25648  cmetcaulem  25653  caussi  25662  causs  25663  lmclimf  25669  mbff  25990  ismbf  25993  ismbfcn  25994  mbfconst  25998  mbfres  26009  mbfimaopn2  26022  cncombf  26023  cnmbf  26024  0plef  26037  0pledm  26038  itg1ge0  26051  mbfi1fseqlem5  26084  itg2addlem  26123  limcfval  26236  limcrcl  26238  ellimc2  26241  limcflf  26245  limcres  26250  limcun  26259  dvfval  26261  dvbss  26265  dvbsss  26266  perfdvf  26267  dvreslem  26273  dvres2lem  26274  dvcnp2  26284  dvnfval  26286  dvnff  26287  dvnf  26291  dvnbss  26292  dvnadd  26293  dvn2bss  26294  dvnres  26295  cpnfval  26296  cpnord  26299  dvaddbr  26302  dvmulbr  26303  dvnfre  26316  dvexp  26317  dvef  26344  c1liplem1  26360  c1lip2  26362  lhop1lem  26377  plyval  26555  elply  26557  elply2  26558  plyf  26560  plyss  26561  elplyr  26563  plyeq0lem  26573  plyeq0  26574  plypf1  26575  plyaddlem1  26576  plymullem1  26577  plyaddlem  26578  plymullem  26579  plysub  26582  coeeulem  26587  coeeq  26590  dgrlem  26592  coeidlem  26600  plyco  26604  coe0  26619  coesub  26620  dgrmulc  26634  dgrsub  26635  dgrcolem1  26636  dgrcolem2  26637  plymul0or  26643  plymul02  26645  plyn0mulidp  26646  dvnply2  26652  plycpn  26654  plydivlem3  26660  plydivlem4  26661  plydiveu  26663  plyremlem  26669  plyrem  26670  facth  26671  fta1lem  26672  rnplynfin  26674  quotcan  26676  vieta1lem2  26678  plyexmo  26680  rngunsnply  26682  elqaalem3  26690  qaa  26693  iaaOLD  26698  aannenlem1  26701  aannenlem2  26702  aannenlem3  26703  taylfvallem1  26730  taylfval  26732  tayl0  26735  taylplem1  26736  taylply2  26741  taylply  26742  dvtaylp  26743  dvntaylp  26744  dvntaylp0  26745  taylthlem1  26746  taylthlem2  26747  ulmval  26753  ulmss  26770  ulmcn  26772  mtest  26777  pserulm  26795  psercn  26799  pserdvlem2  26801  abelth  26814  reefgim  26823  cxpcn2  27120  logbmpt  27162  logbfval  27164  lgamgulmlem5  27406  lgamgulmlem6  27407  lgamgulm2  27409  lgamcvglem  27413  ftalem7  27452  dchrfi  27628  cffldtocusgr  30074  isvcOLD  31227  cnaddabloOLD  31229  cnnvg  31326  cnnvs  31328  cnnvnm  31329  cncph  31467  hvmulex  31659  hfsmval  32386  hfmmval  32387  nmfnval  32524  nlfnval  32529  elcnfn  32530  ellnfn  32531  specval  32546  hhcnf  32553  constrsuc  34474  lmlim  34683  esumcvg  34822  signsplypnf  35283  signsply0  35284  breprexplemb  35364  breprexpnat  35367  vtsval  35370  circlemethnat  35374  circlevma  35375  circlemethhgt  35376  cvxpconn  36208  fwddifval  37135  fwddifnval  37136  ivthALT  37331  knoppcnlem5  37571  knoppcnlem8  37574  bj-inftyexpiinv  38390  bj-inftyexpidisj  38392  caures  38953  cntotbnd  38989  cnpwstotbnd  38990  rrnval  39020  cnaddcom  40288  subex  43558  absex  43559  cjex  43560  elmnc  44397  mpaaeu  44411  itgoval  44422  itgocn  44425  binomcxplemnotnn0  45595  climexp  46884  xlimbr  47104  fuzxrpmcn  47105  xlimmnfvlem2  47110  xlimpnfvlem2  47114  mulcncff  47147  subcncff  47157  addcncff  47161  cncfuni  47163  divcncff  47168  dvsinax  47190  dvcosax  47203  dvnmptdivc  47215  dvnmptconst  47218  dvnxpaek  47219  dvnmul  47220  dvnprodlem3  47225  etransclem1  47512  etransclem2  47513  etransclem4  47515  etransclem13  47524  etransclem46  47557  sqrtnnaa  48180  sqrtnzqaa  48181  numtowerdt  48183  cjnpoly  48206  linplyfv  49705  linply2cfv  49706  linply  49707  lazval  49719  fdivpm  49980  amgmlemALT  51410