Theorem cnex 11182

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

Assertion

Ref	Expression
cnex	⊢ ℂ ∈ V

Proof of Theorem cnex

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

Syntax hints:   ∈ wcel 2143  Vcvv 3455  ℂcc 11099

This theorem was proved from axioms:  ax-cnex 11157

This theorem is referenced by:  reex  11192  cnelprrecn  11194  pnfex  11263  nnex  12240  zex  12601  qex  12986  mpoaddex  13013  addex  13014  mpomulex  13015  mulex  13016  rlim  15548  rlimf  15554  rlimss  15555  elo12  15580  o1f  15582  o1dm  15583  cnso  16304  cnaddablx  19939  cnaddabl  19940  cnaddid  19941  cnaddinv  19942  cnfldbas  21507  cnfldcj  21512  cnfldds  21515  cnfldfun  21517  cnfldfunALT  21518  cnmsubglem  21561  cnmsgngrp  21710  psgninv  21713  lmbrf  23398  lmfss  23434  lmres  23438  lmcnp  23442  cnmet  24909  cncfval  25028  elcncf  25029  cncfcnvcn  25065  cnheibor  25095  cnlmodlem1  25276  tcphex  25357  tchnmfval  25368  tcphcph  25377  lmmbr2  25399  lmmbrf  25402  iscau2  25417  iscauf  25420  caucfil  25423  cmetcaulem  25428  caussi  25437  causs  25438  lmclimf  25444  mbff  25765  ismbf  25768  ismbfcn  25769  mbfconst  25773  mbfres  25784  mbfimaopn2  25797  cncombf  25798  cnmbf  25799  0plef  25812  0pledm  25813  itg1ge0  25826  mbfi1fseqlem5  25859  itg2addlem  25898  limcfval  26012  limcrcl  26014  ellimc2  26017  limcflf  26021  limcres  26026  limcun  26035  dvfval  26037  dvbss  26041  dvbsss  26042  perfdvf  26043  dvreslem  26049  dvres2lem  26050  dvcnp2  26060  dvnfval  26062  dvnff  26063  dvnf  26067  dvnbss  26068  dvnadd  26069  dvn2bss  26070  dvnres  26071  cpnfval  26072  cpnord  26075  dvaddbr  26078  dvmulbr  26079  dvnfre  26092  dvexp  26093  dvef  26120  c1liplem1  26136  c1lip2  26138  lhop1lem  26153  plyval  26331  elply  26333  elply2  26334  plyf  26336  plyss  26337  elplyr  26339  plyeq0lem  26348  plyeq0  26349  plypf1  26350  plyaddlem1  26351  plymullem1  26352  plyaddlem  26353  plymullem  26354  plysub  26357  coeeulem  26362  coeeq  26365  dgrlem  26367  coeidlem  26375  plyco  26379  coe0  26394  coesub  26395  dgrmulc  26409  dgrsub  26410  dgrcolem1  26411  dgrcolem2  26412  plymul0or  26420  plymul02  26422  plyn0mulidp  26423  dvnply2  26429  plycpn  26431  plydivlem3  26437  plydivlem4  26438  plydiveu  26440  plyremlem  26446  plyrem  26447  facth  26448  fta1lem  26449  quotcan  26451  vieta1lem2  26453  plyexmo  26455  elqaalem3  26463  qaa  26465  iaa  26469  aannenlem1  26472  aannenlem2  26473  aannenlem3  26474  taylfvallem1  26501  taylfval  26503  tayl0  26506  taylplem1  26507  taylply2  26512  taylply  26513  dvtaylp  26514  dvntaylp  26515  dvntaylp0  26516  taylthlem1  26517  taylthlem2  26518  ulmval  26524  ulmss  26541  ulmcn  26543  mtest  26548  pserulm  26566  psercn  26570  pserdvlem2  26572  abelth  26585  reefgim  26594  cxpcn2  26892  logbmpt  26934  logbfval  26936  lgamgulmlem5  27178  lgamgulmlem6  27179  lgamgulm2  27181  lgamcvglem  27185  ftalem7  27224  dchrfi  27400  cffldtocusgr  29778  isvcOLD  30912  cnaddabloOLD  30914  cnnvg  31011  cnnvs  31013  cnnvnm  31014  cncph  31152  hvmulex  31344  hfsmval  32071  hfmmval  32072  nmfnval  32209  nlfnval  32214  elcnfn  32215  ellnfn  32216  specval  32231  hhcnf  32238  constrsuc  34109  lmlim  34318  esumcvg  34457  signsplypnf  34918  signsply0  34919  breprexplemb  34999  breprexpnat  35002  vtsval  35005  circlemethnat  35009  circlevma  35010  circlemethhgt  35011  cvxpconn  35715  fwddifval  36635  fwddifnval  36636  ivthALT  36827  knoppcnlem5  37067  knoppcnlem8  37070  bj-inftyexpiinv  37833  bj-inftyexpidisj  37835  caures  38392  cntotbnd  38428  cnpwstotbnd  38429  rrnval  38459  cnaddcom  39727  subex  42996  absex  42997  cjex  42998  elmnc  43846  mpaaeu  43860  itgoval  43871  itgocn  43874  rngunsnply  43879  binomcxplemnotnn0  45049  climexp  46304  xlimbr  46524  fuzxrpmcn  46525  xlimmnfvlem2  46530  xlimpnfvlem2  46534  mulcncff  46567  subcncff  46577  addcncff  46581  cncfuni  46583  divcncff  46588  dvsinax  46610  dvcosax  46623  dvnmptdivc  46635  dvnmptconst  46638  dvnxpaek  46639  dvnmul  46640  dvnprodlem3  46645  etransclem1  46932  etransclem2  46933  etransclem4  46935  etransclem13  46944  etransclem46  46977  sqrtnnaa  47587  sqrtnzqaa  47588  nthrucw  47590  cjnpoly  47609  fdivpm  49306  amgmlemALT  50586