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  9310  zex  9653  qex  10032  addex  10052  mulex  10053  ovshftex  11584  cndsex  14890  cnfldstr  14895  cnfldbas  14897  mpocnfldadd  14898  mpocnfldmul  14900  cnfldcj  14902  expghmap  14942  lmfval  15294  lmbrf  15316  lmfss  15345  lmres  15349  lmtopcnp  15351  cnmet  15631  cncfval  15673  elcncf  15674  limcrcl  15759  limccl  15760  ellimc3apf  15761  limccnp2lem  15777  limccnp2cntop  15778  reldvg  15780  dvfvalap  15782  dvbss  15786  dvidlemap  15792  dvidrelem  15793  dvidsslem  15794  dvcnp2cntop  15800  dvaddxxbr  15802  dvmulxxbr  15803  dvaddxx  15804  dvmulxx  15805  dviaddf  15806  dvimulf  15807  dvcoapbr  15808  dvcjbr  15809  dvcj  15810  dvfre  15811  dvexp  15812  dvrecap  15814  dvmptclx  15819  dvef  15828  plyval  15833  elply  15835  elply2  15836  plyf  15838  plyss  15839  elplyr  15841  plyaddlem1  15848  plymullem1  15849  plyaddlem  15850  plymullem  15851  plysub  15854  plycolemc  15859  plyco  15860  plycj  15862