Theorem cnex 8309

Description: Alias for ax-cnex 8276. (Contributed by Mario Carneiro, 17-Nov-2014.)

Assertion

Ref	Expression
cnex	|- CC e. _V

Proof of Theorem cnex

Step	Hyp	Ref	Expression
1		ax-cnex 8276	1 |- CC e. _V

This proof depends on syntax axioms:   e. wcel 2209   _Vcvv 2821   CCcc 8183

This proof depends on axioms:  ax-cnex 8276

This theorem is used by:  reex  8319  cnelprrecn  8321  pnfnre  8373  mnfnre  8374  pnfxr  8384  nnex  9319  zex  9664  qex  10048  addex  10069  mulex  10070  ovshftex  11606  cndsex  14999  cnfldstr  15004  cnfldbas  15006  mpocnfldadd  15007  mpocnfldmul  15009  cnfldcj  15011  expghmap  15051  lmfval  15419  lmbrf  15441  lmfss  15470  lmres  15474  lmtopcnp  15476  cnmet  15756  cncfval  15798  elcncf  15799  limcrcl  15884  limccl  15885  ellimc3apf  15886  limccnp2lem  15902  limccnp2cntop  15903  reldvg  15905  dvfvalap  15907  dvbss  15911  dvidlemap  15917  dvidrelem  15918  dvidsslem  15919  dvcnp2cntop  15925  dvaddxxbr  15927  dvmulxxbr  15928  dvaddxx  15929  dvmulxx  15930  dviaddf  15931  dvimulf  15932  dvcoapbr  15933  dvcjbr  15934  dvcj  15935  dvfre  15936  dvexp  15937  dvrecap  15939  dvmptclx  15944  dvef  15953  plyval  15958  elply  15960  elply2  15961  plyf  15963  plyss  15964  elplyr  15966  plyaddlem1  15973  plymullem1  15974  plyaddlem  15975  plymullem  15976  plysub  15979  plycolemc  15984  plyco  15985  plycj  15987