ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  cnex GIF version

Theorem cnex 8199
Description: Alias for ax-cnex 8166. (Contributed by Mario Carneiro, 17-Nov-2014.)
Assertion
Ref Expression
cnex ℂ ∈ V

Proof of Theorem cnex
StepHypRef Expression
1 ax-cnex 8166 1 ℂ ∈ V
Colors of variables: wff set class
Syntax hints:  wcel 2202  Vcvv 2803  cc 8073
This theorem was proved from axioms:  ax-cnex 8166
This theorem is referenced by:  reex  8209  cnelprrecn  8211  pnfnre  8263  mnfnre  8264  pnfxr  8274  nnex  9191  zex  9532  qex  9910  addex  9930  mulex  9931  ovshftex  11442  cndsex  14632  cnfldstr  14637  cnfldbas  14639  mpocnfldadd  14640  mpocnfldmul  14642  cnfldcj  14644  expghmap  14686  lmfval  14987  lmbrf  15009  lmfss  15038  lmres  15042  lmtopcnp  15044  cnmet  15324  cncfval  15366  elcncf  15367  limcrcl  15452  limccl  15453  ellimc3apf  15454  limccnp2lem  15470  limccnp2cntop  15471  reldvg  15473  dvfvalap  15475  dvbss  15479  dvidlemap  15485  dvidrelem  15486  dvidsslem  15487  dvcnp2cntop  15493  dvaddxxbr  15495  dvmulxxbr  15496  dvaddxx  15497  dvmulxx  15498  dviaddf  15499  dvimulf  15500  dvcoapbr  15501  dvcjbr  15502  dvcj  15503  dvfre  15504  dvexp  15505  dvrecap  15507  dvmptclx  15512  dvef  15521  plyval  15526  elply  15528  elply2  15529  plyf  15531  plyss  15532  elplyr  15534  plyaddlem1  15541  plymullem1  15542  plyaddlem  15543  plymullem  15544  plysub  15547  plycolemc  15552  plyco  15553  plycj  15555
  Copyright terms: Public domain W3C validator