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

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

Proof of Theorem cnex
StepHypRef Expression
1 ax-cnex 8101 1 ℂ ∈ V
Colors of variables: wff set class
Syntax hints:  wcel 2200  Vcvv 2799  cc 8008
This theorem was proved from axioms:  ax-cnex 8101
This theorem is referenced by:  reex  8144  cnelprrecn  8146  pnfnre  8199  mnfnre  8200  pnfxr  8210  nnex  9127  zex  9466  qex  9839  addex  9859  mulex  9860  ovshftex  11345  cndsex  14532  cnfldstr  14537  cnfldbas  14539  mpocnfldadd  14540  mpocnfldmul  14542  cnfldcj  14544  expghmap  14586  lmfval  14882  lmbrf  14904  lmfss  14933  lmres  14937  lmtopcnp  14939  cnmet  15219  cncfval  15261  elcncf  15262  limcrcl  15347  limccl  15348  ellimc3apf  15349  limccnp2lem  15365  limccnp2cntop  15366  reldvg  15368  dvfvalap  15370  dvbss  15374  dvidlemap  15380  dvidrelem  15381  dvidsslem  15382  dvcnp2cntop  15388  dvaddxxbr  15390  dvmulxxbr  15391  dvaddxx  15392  dvmulxx  15393  dviaddf  15394  dvimulf  15395  dvcoapbr  15396  dvcjbr  15397  dvcj  15398  dvfre  15399  dvexp  15400  dvrecap  15402  dvmptclx  15407  dvef  15416  plyval  15421  elply  15423  elply2  15424  plyf  15426  plyss  15427  elplyr  15429  plyaddlem1  15436  plymullem1  15437  plyaddlem  15438  plymullem  15439  plysub  15442  plycolemc  15447  plyco  15448  plycj  15450
  Copyright terms: Public domain W3C validator