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

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

Proof of Theorem cnex
StepHypRef Expression
1 ax-cnex 7704 1  |-  CC  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 1480   _Vcvv 2681   CCcc 7611
This theorem was proved from axioms:  ax-cnex 7704
This theorem is referenced by:  reex  7747  cnelprrecn  7749  pnfnre  7800  mnfnre  7801  pnfxr  7811  nnex  8719  zex  9056  qex  9417  ovshftex  10584  lmfval  12350  lmbrf  12373  lmfss  12402  lmres  12406  lmtopcnp  12408  cnmet  12688  cncfval  12717  elcncf  12718  limcrcl  12785  limccl  12786  ellimc3apf  12787  limccnp2lem  12803  limccnp2cntop  12804  reldvg  12806  dvfvalap  12808  dvbss  12812  dvidlemap  12818  dvcnp2cntop  12821  dvaddxxbr  12823  dvmulxxbr  12824  dvaddxx  12825  dvmulxx  12826  dviaddf  12827  dvimulf  12828  dvcoapbr  12829  dvcjbr  12830  dvcj  12831  dvfre  12832  dvexp  12833  dvrecap  12835  dvmptclx  12838  dvef  12845
  Copyright terms: Public domain W3C validator