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

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

Proof of Theorem cnex
StepHypRef Expression
1 ax-cnex 7901 1  |-  CC  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 2148   _Vcvv 2737   CCcc 7808
This theorem was proved from axioms:  ax-cnex 7901
This theorem is referenced by:  reex  7944  cnelprrecn  7946  pnfnre  7997  mnfnre  7998  pnfxr  8008  nnex  8923  zex  9260  qex  9630  addex  9649  mulex  9650  ovshftex  10823  cnfldstr  13388  cnfldbas  13390  cnfldcj  13393  lmfval  13623  lmbrf  13646  lmfss  13675  lmres  13679  lmtopcnp  13681  cnmet  13961  cncfval  13990  elcncf  13991  limcrcl  14058  limccl  14059  ellimc3apf  14060  limccnp2lem  14076  limccnp2cntop  14077  reldvg  14079  dvfvalap  14081  dvbss  14085  dvidlemap  14091  dvcnp2cntop  14094  dvaddxxbr  14096  dvmulxxbr  14097  dvaddxx  14098  dvmulxx  14099  dviaddf  14100  dvimulf  14101  dvcoapbr  14102  dvcjbr  14103  dvcj  14104  dvfre  14105  dvexp  14106  dvrecap  14108  dvmptclx  14111  dvef  14119
  Copyright terms: Public domain W3C validator