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

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

Proof of Theorem cnex
StepHypRef Expression
1 ax-cnex 7970 1 ℂ ∈ V
Colors of variables: wff set class
Syntax hints:  wcel 2167  Vcvv 2763  cc 7877
This theorem was proved from axioms:  ax-cnex 7970
This theorem is referenced by:  reex  8013  cnelprrecn  8015  pnfnre  8068  mnfnre  8069  pnfxr  8079  nnex  8996  zex  9335  qex  9706  addex  9726  mulex  9727  ovshftex  10984  cndsex  14109  cnfldstr  14114  cnfldbas  14116  mpocnfldadd  14117  mpocnfldmul  14119  cnfldcj  14121  expghmap  14163  lmfval  14428  lmbrf  14451  lmfss  14480  lmres  14484  lmtopcnp  14486  cnmet  14766  cncfval  14808  elcncf  14809  limcrcl  14894  limccl  14895  ellimc3apf  14896  limccnp2lem  14912  limccnp2cntop  14913  reldvg  14915  dvfvalap  14917  dvbss  14921  dvidlemap  14927  dvidrelem  14928  dvidsslem  14929  dvcnp2cntop  14935  dvaddxxbr  14937  dvmulxxbr  14938  dvaddxx  14939  dvmulxx  14940  dviaddf  14941  dvimulf  14942  dvcoapbr  14943  dvcjbr  14944  dvcj  14945  dvfre  14946  dvexp  14947  dvrecap  14949  dvmptclx  14954  dvef  14963  plyval  14968  elply  14970  elply2  14971  plyf  14973  plyss  14974  elplyr  14976  plyaddlem1  14983  plymullem1  14984  plyaddlem  14985  plymullem  14986  plysub  14989  plycolemc  14994  plyco  14995  plycj  14997
  Copyright terms: Public domain W3C validator