Theorem cnex 11205

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

Assertion

Ref	Expression
cnex	⊢ ℂ ∈ V

Proof of Theorem cnex

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

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3450  ℂcc 11122

This proof depends on axioms:  ax-cnex 11180

This theorem is used by:  reex  11215  cnelprrecn  11217  pnfex  11286  nnex  12263  zex  12624  qex  13010  mpoaddex  13038  addex  13039  mpomulex  13040  mulex  13041  rlim  15582  rlimf  15588  rlimss  15589  elo12  15614  o1f  15616  o1dm  15617  cnso  16335  cnaddablx  19995  cnaddabl  19996  cnaddid  19997  cnaddinv  19998  cnfldbas  21589  cnfldcj  21594  cnfldds  21597  cnfldfun  21599  cnfldfunALT  21600  cnmsubglem  21643  cnmsgngrp  21792  psgninv  21795  lmbrf  23485  lmfss  23521  lmres  23525  lmcnp  23529  cnmet  24997  cncfval  25116  elcncf  25117  cncfcnvcn  25153  cnheibor  25183  cnlmodlem1  25364  tcphex  25445  tchnmfval  25456  tcphcph  25465  lmmbr2  25487  lmmbrf  25490  iscau2  25505  iscauf  25508  caucfil  25511  cmetcaulem  25516  caussi  25525  causs  25526  lmclimf  25532  mbff  25853  ismbf  25856  ismbfcn  25857  mbfconst  25861  mbfres  25872  mbfimaopn2  25885  cncombf  25886  cnmbf  25887  0plef  25900  0pledm  25901  itg1ge0  25914  mbfi1fseqlem5  25947  itg2addlem  25986  limcfval  26099  limcrcl  26101  ellimc2  26104  limcflf  26108  limcres  26113  limcun  26122  dvfval  26124  dvbss  26128  dvbsss  26129  perfdvf  26130  dvreslem  26136  dvres2lem  26137  dvcnp2  26147  dvnfval  26149  dvnff  26150  dvnf  26154  dvnbss  26155  dvnadd  26156  dvn2bss  26157  dvnres  26158  cpnfval  26159  cpnord  26162  dvaddbr  26165  dvmulbr  26166  dvnfre  26179  dvexp  26180  dvef  26207  c1liplem1  26223  c1lip2  26225  lhop1lem  26240  plyval  26418  elply  26420  elply2  26421  plyf  26423  plyss  26424  elplyr  26426  plyeq0lem  26436  plyeq0  26437  plypf1  26438  plyaddlem1  26439  plymullem1  26440  plyaddlem  26441  plymullem  26442  plysub  26445  coeeulem  26450  coeeq  26453  dgrlem  26455  coeidlem  26463  plyco  26467  coe0  26482  coesub  26483  dgrmulc  26497  dgrsub  26498  dgrcolem1  26499  dgrcolem2  26500  plymul0or  26508  plymul02  26510  plyn0mulidp  26511  dvnply2  26517  plycpn  26519  plydivlem3  26525  plydivlem4  26526  plydiveu  26528  plyremlem  26534  plyrem  26535  facth  26536  fta1lem  26537  rnplynfin  26539  quotcan  26541  vieta1lem2  26543  plyexmo  26545  elqaalem3  26553  qaa  26556  iaaOLD  26561  aannenlem1  26564  aannenlem2  26565  aannenlem3  26566  taylfvallem1  26593  taylfval  26595  tayl0  26598  taylplem1  26599  taylply2  26604  taylply  26605  dvtaylp  26606  dvntaylp  26607  dvntaylp0  26608  taylthlem1  26609  taylthlem2  26610  ulmval  26616  ulmss  26633  ulmcn  26635  mtest  26640  pserulm  26658  psercn  26662  pserdvlem2  26664  abelth  26677  reefgim  26686  cxpcn2  26983  logbmpt  27025  logbfval  27027  lgamgulmlem5  27269  lgamgulmlem6  27270  lgamgulm2  27272  lgamcvglem  27276  ftalem7  27315  dchrfi  27491  cffldtocusgr  29907  isvcOLD  31060  cnaddabloOLD  31062  cnnvg  31159  cnnvs  31161  cnnvnm  31162  cncph  31300  hvmulex  31492  hfsmval  32219  hfmmval  32220  nmfnval  32357  nlfnval  32362  elcnfn  32363  ellnfn  32364  specval  32379  hhcnf  32386  constrsuc  34248  lmlim  34457  esumcvg  34596  signsplypnf  35058  signsply0  35059  breprexplemb  35139  breprexpnat  35142  vtsval  35145  circlemethnat  35149  circlevma  35150  circlemethhgt  35151  cvxpconn  35821  fwddifval  36742  fwddifnval  36743  ivthALT  36954  knoppcnlem5  37194  knoppcnlem8  37197  bj-inftyexpiinv  37960  bj-inftyexpidisj  37962  caures  38510  cntotbnd  38546  cnpwstotbnd  38547  rrnval  38577  cnaddcom  39845  subex  43114  absex  43115  cjex  43116  elmnc  43977  mpaaeu  43991  itgoval  44002  itgocn  44005  rngunsnply  44010  binomcxplemnotnn0  45180  climexp  46435  xlimbr  46655  fuzxrpmcn  46656  xlimmnfvlem2  46661  xlimpnfvlem2  46665  mulcncff  46698  subcncff  46708  addcncff  46712  cncfuni  46714  divcncff  46719  dvsinax  46741  dvcosax  46754  dvnmptdivc  46766  dvnmptconst  46769  dvnxpaek  46770  dvnmul  46771  dvnprodlem3  46776  etransclem1  47063  etransclem2  47064  etransclem4  47066  etransclem13  47075  etransclem46  47108  sqrtnnaa  47731  sqrtnzqaa  47732  numtowerdt  47734  cjnpoly  47757  fdivpm  49473  amgmlemALT  50821