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

Theorem cnex 8134
Description: Alias for ax-cnex 8101. (Contributed by Mario Carneiro, 17-Nov-2014.)
Assertion
Ref Expression
cnex  |-  CC  e.  _V

Proof of Theorem cnex
StepHypRef Expression
1 ax-cnex 8101 1  |-  CC  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 2200   _Vcvv 2799   CCcc 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  11346  cndsex  14533  cnfldstr  14538  cnfldbas  14540  mpocnfldadd  14541  mpocnfldmul  14543  cnfldcj  14545  expghmap  14587  lmfval  14883  lmbrf  14905  lmfss  14934  lmres  14938  lmtopcnp  14940  cnmet  15220  cncfval  15262  elcncf  15263  limcrcl  15348  limccl  15349  ellimc3apf  15350  limccnp2lem  15366  limccnp2cntop  15367  reldvg  15369  dvfvalap  15371  dvbss  15375  dvidlemap  15381  dvidrelem  15382  dvidsslem  15383  dvcnp2cntop  15389  dvaddxxbr  15391  dvmulxxbr  15392  dvaddxx  15393  dvmulxx  15394  dviaddf  15395  dvimulf  15396  dvcoapbr  15397  dvcjbr  15398  dvcj  15399  dvfre  15400  dvexp  15401  dvrecap  15403  dvmptclx  15408  dvef  15417  plyval  15422  elply  15424  elply2  15425  plyf  15427  plyss  15428  elplyr  15430  plyaddlem1  15437  plymullem1  15438  plyaddlem  15439  plymullem  15440  plysub  15443  plycolemc  15448  plyco  15449  plycj  15451
  Copyright terms: Public domain W3C validator