Theorem cnex 8020

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

Assertion

Ref	Expression
cnex	⊢ ℂ ∈ V

Proof of Theorem cnex

Step	Hyp	Ref	Expression
1		ax-cnex 7987	1 ⊢ ℂ ∈ V

Syntax hints:   ∈ wcel 2167  Vcvv 2763  ℂcc 7894

This theorem was proved from axioms:  ax-cnex 7987

This theorem is referenced by:  reex  8030  cnelprrecn  8032  pnfnre  8085  mnfnre  8086  pnfxr  8096  nnex  9013  zex  9352  qex  9723  addex  9743  mulex  9744  ovshftex  11001  cndsex  14185  cnfldstr  14190  cnfldbas  14192  mpocnfldadd  14193  mpocnfldmul  14195  cnfldcj  14197  expghmap  14239  lmfval  14512  lmbrf  14535  lmfss  14564  lmres  14568  lmtopcnp  14570  cnmet  14850  cncfval  14892  elcncf  14893  limcrcl  14978  limccl  14979  ellimc3apf  14980  limccnp2lem  14996  limccnp2cntop  14997  reldvg  14999  dvfvalap  15001  dvbss  15005  dvidlemap  15011  dvidrelem  15012  dvidsslem  15013  dvcnp2cntop  15019  dvaddxxbr  15021  dvmulxxbr  15022  dvaddxx  15023  dvmulxx  15024  dviaddf  15025  dvimulf  15026  dvcoapbr  15027  dvcjbr  15028  dvcj  15029  dvfre  15030  dvexp  15031  dvrecap  15033  dvmptclx  15038  dvef  15047  plyval  15052  elply  15054  elply2  15055  plyf  15057  plyss  15058  elplyr  15060  plyaddlem1  15067  plymullem1  15068  plyaddlem  15069  plymullem  15070  plysub  15073  plycolemc  15078  plyco  15079  plycj  15081