Theorem cnex 8303

Description: Alias for ax-cnex 8270. (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 8270	1 |- CC e. _V

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

This proof depends on axioms:  ax-cnex 8270

This theorem is used by:  reex  8313  cnelprrecn  8315  pnfnre  8367  mnfnre  8368  pnfxr  8378  nnex  9312  zex  9657  qex  10041  addex  10062  mulex  10063  ovshftex  11598  cndsex  14939  cnfldstr  14944  cnfldbas  14946  mpocnfldadd  14947  mpocnfldmul  14949  cnfldcj  14951  expghmap  14991  lmfval  15343  lmbrf  15365  lmfss  15394  lmres  15398  lmtopcnp  15400  cnmet  15680  cncfval  15722  elcncf  15723  limcrcl  15808  limccl  15809  ellimc3apf  15810  limccnp2lem  15826  limccnp2cntop  15827  reldvg  15829  dvfvalap  15831  dvbss  15835  dvidlemap  15841  dvidrelem  15842  dvidsslem  15843  dvcnp2cntop  15849  dvaddxxbr  15851  dvmulxxbr  15852  dvaddxx  15853  dvmulxx  15854  dviaddf  15855  dvimulf  15856  dvcoapbr  15857  dvcjbr  15858  dvcj  15859  dvfre  15860  dvexp  15861  dvrecap  15863  dvmptclx  15868  dvef  15877  plyval  15882  elply  15884  elply2  15885  plyf  15887  plyss  15888  elplyr  15890  plyaddlem1  15897  plymullem1  15898  plyaddlem  15899  plymullem  15900  plysub  15903  plycolemc  15908  plyco  15909  plycj  15911