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

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

Proof of Theorem cnex
StepHypRef Expression
1 ax-cnex 7973 1 ℂ ∈ V
Colors of variables: wff set class
Syntax hints:  wcel 2167  Vcvv 2763  cc 7880
This theorem was proved from axioms:  ax-cnex 7973
This theorem is referenced by:  reex  8016  cnelprrecn  8018  pnfnre  8071  mnfnre  8072  pnfxr  8082  nnex  8999  zex  9338  qex  9709  addex  9729  mulex  9730  ovshftex  10987  cndsex  14135  cnfldstr  14140  cnfldbas  14142  mpocnfldadd  14143  mpocnfldmul  14145  cnfldcj  14147  expghmap  14189  lmfval  14454  lmbrf  14477  lmfss  14506  lmres  14510  lmtopcnp  14512  cnmet  14792  cncfval  14834  elcncf  14835  limcrcl  14920  limccl  14921  ellimc3apf  14922  limccnp2lem  14938  limccnp2cntop  14939  reldvg  14941  dvfvalap  14943  dvbss  14947  dvidlemap  14953  dvidrelem  14954  dvidsslem  14955  dvcnp2cntop  14961  dvaddxxbr  14963  dvmulxxbr  14964  dvaddxx  14965  dvmulxx  14966  dviaddf  14967  dvimulf  14968  dvcoapbr  14969  dvcjbr  14970  dvcj  14971  dvfre  14972  dvexp  14973  dvrecap  14975  dvmptclx  14980  dvef  14989  plyval  14994  elply  14996  elply2  14997  plyf  14999  plyss  15000  elplyr  15002  plyaddlem1  15009  plymullem1  15010  plyaddlem  15011  plymullem  15012  plysub  15015  plycolemc  15020  plyco  15021  plycj  15023
  Copyright terms: Public domain W3C validator