Theorem cnex 8304

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

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

This proof depends on axioms:  ax-cnex 8271

This theorem is used by:  reex  8314  cnelprrecn  8316  pnfnre  8368  mnfnre  8369  pnfxr  8379  nnex  9313  zex  9658  qex  10042  addex  10063  mulex  10064  ovshftex  11600  cndsex  14981  cnfldstr  14986  cnfldbas  14988  mpocnfldadd  14989  mpocnfldmul  14991  cnfldcj  14993  expghmap  15033  lmfval  15393  lmbrf  15415  lmfss  15444  lmres  15448  lmtopcnp  15450  cnmet  15730  cncfval  15772  elcncf  15773  limcrcl  15858  limccl  15859  ellimc3apf  15860  limccnp2lem  15876  limccnp2cntop  15877  reldvg  15879  dvfvalap  15881  dvbss  15885  dvidlemap  15891  dvidrelem  15892  dvidsslem  15893  dvcnp2cntop  15899  dvaddxxbr  15901  dvmulxxbr  15902  dvaddxx  15903  dvmulxx  15904  dviaddf  15905  dvimulf  15906  dvcoapbr  15907  dvcjbr  15908  dvcj  15909  dvfre  15910  dvexp  15911  dvrecap  15913  dvmptclx  15918  dvef  15927  plyval  15932  elply  15934  elply2  15935  plyf  15937  plyss  15938  elplyr  15940  plyaddlem1  15947  plymullem1  15948  plyaddlem  15949  plymullem  15950  plysub  15953  plycolemc  15958  plyco  15959  plycj  15961