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

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

Proof of Theorem cnex
StepHypRef Expression
1 ax-cnex 7199 1  |-  CC  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 1434   _Vcvv 2610   CCcc 7111
This theorem was proved from axioms:  ax-cnex 7199
This theorem is referenced by:  reex  7239  cnelprrecn  7241  pnfnre  7292  mnfnre  7293  pnfxr  7303  nnex  8182  zex  8511  qex  8868  iseradd  9629  isersub  9630  serige0  9640  serile  9641  ibcval5  9857  ovshftex  9926  clim2iser  10394  clim2iser2  10395  iisermulc2  10397  iserile  10399  climserile  10402  fisumcvg  10419
  Copyright terms: Public domain W3C validator