Theorem cnex 11192

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

Assertion

Ref	Expression
cnex	⊢ ℂ ∈ V

Proof of Theorem cnex

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

This proof depends on syntax axioms:   ∈ wcel 2146  Vcvv 3457  ℂcc 11109

This proof depends on axioms:  ax-cnex 11167

This theorem is used by:  reex  11202  cnelprrecn  11204  pnfex  11273  nnex  12250  zex  12611  qex  12997  mpoaddex  13024  addex  13025  mpomulex  13026  mulex  13027  rlim  15566  rlimf  15572  rlimss  15573  elo12  15598  o1f  15600  o1dm  15601  cnso  16321  cnaddablx  19962  cnaddabl  19963  cnaddid  19964  cnaddinv  19965  cnfldbas  21556  cnfldcj  21561  cnfldds  21564  cnfldfun  21566  cnfldfunALT  21567  cnmsubglem  21610  cnmsgngrp  21759  psgninv  21762  lmbrf  23447  lmfss  23483  lmres  23487  lmcnp  23491  cnmet  24959  cncfval  25078  elcncf  25079  cncfcnvcn  25115  cnheibor  25145  cnlmodlem1  25326  tcphex  25407  tchnmfval  25418  tcphcph  25427  lmmbr2  25449  lmmbrf  25452  iscau2  25467  iscauf  25470  caucfil  25473  cmetcaulem  25478  caussi  25487  causs  25488  lmclimf  25494  mbff  25815  ismbf  25818  ismbfcn  25819  mbfconst  25823  mbfres  25834  mbfimaopn2  25847  cncombf  25848  cnmbf  25849  0plef  25862  0pledm  25863  itg1ge0  25876  mbfi1fseqlem5  25909  itg2addlem  25948  limcfval  26062  limcrcl  26064  ellimc2  26067  limcflf  26071  limcres  26076  limcun  26085  dvfval  26087  dvbss  26091  dvbsss  26092  perfdvf  26093  dvreslem  26099  dvres2lem  26100  dvcnp2  26110  dvnfval  26112  dvnff  26113  dvnf  26117  dvnbss  26118  dvnadd  26119  dvn2bss  26120  dvnres  26121  cpnfval  26122  cpnord  26125  dvaddbr  26128  dvmulbr  26129  dvnfre  26142  dvexp  26143  dvef  26170  c1liplem1  26186  c1lip2  26188  lhop1lem  26203  plyval  26381  elply  26383  elply2  26384  plyf  26386  plyss  26387  elplyr  26389  plyeq0lem  26398  plyeq0  26399  plypf1  26400  plyaddlem1  26401  plymullem1  26402  plyaddlem  26403  plymullem  26404  plysub  26407  coeeulem  26412  coeeq  26415  dgrlem  26417  coeidlem  26425  plyco  26429  coe0  26444  coesub  26445  dgrmulc  26459  dgrsub  26460  dgrcolem1  26461  dgrcolem2  26462  plymul0or  26470  plymul02  26472  plyn0mulidp  26473  dvnply2  26479  plycpn  26481  plydivlem3  26487  plydivlem4  26488  plydiveu  26490  plyremlem  26496  plyrem  26497  facth  26498  fta1lem  26499  quotcan  26501  vieta1lem2  26503  plyexmo  26505  elqaalem3  26513  qaa  26515  iaa  26519  aannenlem1  26522  aannenlem2  26523  aannenlem3  26524  taylfvallem1  26551  taylfval  26553  tayl0  26556  taylplem1  26557  taylply2  26562  taylply  26563  dvtaylp  26564  dvntaylp  26565  dvntaylp0  26566  taylthlem1  26567  taylthlem2  26568  ulmval  26574  ulmss  26591  ulmcn  26593  mtest  26598  pserulm  26616  psercn  26620  pserdvlem2  26622  abelth  26635  reefgim  26644  cxpcn2  26942  logbmpt  26984  logbfval  26986  lgamgulmlem5  27228  lgamgulmlem6  27229  lgamgulm2  27231  lgamcvglem  27235  ftalem7  27274  dchrfi  27450  cffldtocusgr  29831  isvcOLD  30978  cnaddabloOLD  30980  cnnvg  31077  cnnvs  31079  cnnvnm  31080  cncph  31218  hvmulex  31410  hfsmval  32137  hfmmval  32138  nmfnval  32275  nlfnval  32280  elcnfn  32281  ellnfn  32282  specval  32297  hhcnf  32304  constrsuc  34168  lmlim  34377  esumcvg  34516  signsplypnf  34978  signsply0  34979  breprexplemb  35059  breprexpnat  35062  vtsval  35065  circlemethnat  35069  circlevma  35070  circlemethhgt  35071  cvxpconn  35747  fwddifval  36667  fwddifnval  36668  ivthALT  36879  knoppcnlem5  37119  knoppcnlem8  37122  bj-inftyexpiinv  37885  bj-inftyexpidisj  37887  caures  38444  cntotbnd  38480  cnpwstotbnd  38481  rrnval  38511  cnaddcom  39779  subex  43048  absex  43049  cjex  43050  elmnc  43896  mpaaeu  43910  itgoval  43921  itgocn  43924  rngunsnply  43929  binomcxplemnotnn0  45099  climexp  46354  xlimbr  46574  fuzxrpmcn  46575  xlimmnfvlem2  46580  xlimpnfvlem2  46584  mulcncff  46617  subcncff  46627  addcncff  46631  cncfuni  46633  divcncff  46638  dvsinax  46660  dvcosax  46673  dvnmptdivc  46685  dvnmptconst  46688  dvnxpaek  46689  dvnmul  46690  dvnprodlem3  46695  etransclem1  46982  etransclem2  46983  etransclem4  46985  etransclem13  46994  etransclem46  47027  sqrtnnaa  47637  sqrtnzqaa  47638  nthrucw  47640  cjnpoly  47659  fdivpm  49356  amgmlemALT  50684