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

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

Proof of Theorem cnex
StepHypRef Expression
1 ax-cnex 8260 1 ℂ ∈ V
Colors of variables: wff set class
Syntax hints:  wcel 2209  Vcvv 2821  cc 8167
This theorem was proved from axioms:  ax-cnex 8260
This theorem is referenced by:  reex  8303  cnelprrecn  8305  pnfnre  8357  mnfnre  8358  pnfxr  8368  nnex  9289  zex  9632  qex  10011  addex  10031  mulex  10032  ovshftex  11562  cndsex  14862  cnfldstr  14867  cnfldbas  14869  mpocnfldadd  14870  mpocnfldmul  14872  cnfldcj  14874  expghmap  14914  lmfval  15217  lmbrf  15239  lmfss  15268  lmres  15272  lmtopcnp  15274  cnmet  15554  cncfval  15596  elcncf  15597  limcrcl  15682  limccl  15683  ellimc3apf  15684  limccnp2lem  15700  limccnp2cntop  15701  reldvg  15703  dvfvalap  15705  dvbss  15709  dvidlemap  15715  dvidrelem  15716  dvidsslem  15717  dvcnp2cntop  15723  dvaddxxbr  15725  dvmulxxbr  15726  dvaddxx  15727  dvmulxx  15728  dviaddf  15729  dvimulf  15730  dvcoapbr  15731  dvcjbr  15732  dvcj  15733  dvfre  15734  dvexp  15735  dvrecap  15737  dvmptclx  15742  dvef  15751  plyval  15756  elply  15758  elply2  15759  plyf  15761  plyss  15762  elplyr  15764  plyaddlem1  15771  plymullem1  15772  plyaddlem  15773  plymullem  15774  plysub  15777  plycolemc  15782  plyco  15783  plycj  15785
  Copyright terms: Public domain W3C validator