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

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

Proof of Theorem cnex
StepHypRef Expression
1 ax-cnex 8234 1 ℂ ∈ V
Colors of variables: wff set class
Syntax hints:  wcel 2205  Vcvv 2815  cc 8141
This theorem was proved from axioms:  ax-cnex 8234
This theorem is referenced by:  reex  8277  cnelprrecn  8279  pnfnre  8331  mnfnre  8332  pnfxr  8342  nnex  9260  zex  9603  qex  9982  addex  10002  mulex  10003  ovshftex  11529  cndsex  14827  cnfldstr  14832  cnfldbas  14834  mpocnfldadd  14835  mpocnfldmul  14837  cnfldcj  14839  expghmap  14881  lmfval  15184  lmbrf  15206  lmfss  15235  lmres  15239  lmtopcnp  15241  cnmet  15521  cncfval  15563  elcncf  15564  limcrcl  15649  limccl  15650  ellimc3apf  15651  limccnp2lem  15667  limccnp2cntop  15668  reldvg  15670  dvfvalap  15672  dvbss  15676  dvidlemap  15682  dvidrelem  15683  dvidsslem  15684  dvcnp2cntop  15690  dvaddxxbr  15692  dvmulxxbr  15693  dvaddxx  15694  dvmulxx  15695  dviaddf  15696  dvimulf  15697  dvcoapbr  15698  dvcjbr  15699  dvcj  15700  dvfre  15701  dvexp  15702  dvrecap  15704  dvmptclx  15709  dvef  15718  plyval  15723  elply  15725  elply2  15726  plyf  15728  plyss  15729  elplyr  15731  plyaddlem1  15738  plymullem1  15739  plyaddlem  15740  plymullem  15741  plysub  15744  plycolemc  15749  plyco  15750  plycj  15752
  Copyright terms: Public domain W3C validator