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  9662  qex  10047  addex  10068  mulex  10069  ovshftex  11605  cndsex  14998  cnfldstr  15003  cnfldbas  15005  mpocnfldadd  15006  mpocnfldmul  15008  cnfldcj  15010  expghmap  15050  lmfval  15436  lmbrf  15458  lmfss  15487  lmres  15491  lmtopcnp  15493  cnmet  15773  cncfval  15815  elcncf  15816  limcrcl  15901  limccl  15902  ellimc3apf  15903  limccnp2lem  15919  limccnp2cntop  15920  reldvg  15922  dvfvalap  15924  dvbss  15928  dvidlemap  15934  dvidrelem  15935  dvidsslem  15936  dvcnp2cntop  15942  dvaddxxbr  15944  dvmulxxbr  15945  dvaddxx  15946  dvmulxx  15947  dviaddf  15948  dvimulf  15949  dvcoapbr  15950  dvcjbr  15951  dvcj  15952  dvfre  15953  dvexp  15954  dvrecap  15956  dvmptclx  15961  dvef  15970  plyval  15975  elply  15977  elply2  15978  plyf  15980  plyss  15981  elplyr  15983  plyaddlem1  15990  plymullem1  15991  plyaddlem  15992  plymullem  15993  plysub  15996  plycolemc  16001  plyco  16002  plycj  16004