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

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

Proof of Theorem cnex
StepHypRef Expression
1 ax-cnex 7989 1 ℂ ∈ V
Colors of variables: wff set class
Syntax hints:  wcel 2167  Vcvv 2763  cc 7896
This theorem was proved from axioms:  ax-cnex 7989
This theorem is referenced by:  reex  8032  cnelprrecn  8034  pnfnre  8087  mnfnre  8088  pnfxr  8098  nnex  9015  zex  9354  qex  9725  addex  9745  mulex  9746  ovshftex  11003  cndsex  14187  cnfldstr  14192  cnfldbas  14194  mpocnfldadd  14195  mpocnfldmul  14197  cnfldcj  14199  expghmap  14241  lmfval  14536  lmbrf  14559  lmfss  14588  lmres  14592  lmtopcnp  14594  cnmet  14874  cncfval  14916  elcncf  14917  limcrcl  15002  limccl  15003  ellimc3apf  15004  limccnp2lem  15020  limccnp2cntop  15021  reldvg  15023  dvfvalap  15025  dvbss  15029  dvidlemap  15035  dvidrelem  15036  dvidsslem  15037  dvcnp2cntop  15043  dvaddxxbr  15045  dvmulxxbr  15046  dvaddxx  15047  dvmulxx  15048  dviaddf  15049  dvimulf  15050  dvcoapbr  15051  dvcjbr  15052  dvcj  15053  dvfre  15054  dvexp  15055  dvrecap  15057  dvmptclx  15062  dvef  15071  plyval  15076  elply  15078  elply2  15079  plyf  15081  plyss  15082  elplyr  15084  plyaddlem1  15091  plymullem1  15092  plyaddlem  15093  plymullem  15094  plysub  15097  plycolemc  15102  plyco  15103  plycj  15105
  Copyright terms: Public domain W3C validator