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

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

Proof of Theorem cnex
StepHypRef Expression
1 ax-cnex 7902 1  |-  CC  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 2148   _Vcvv 2738   CCcc 7809
This theorem was proved from axioms:  ax-cnex 7902
This theorem is referenced by:  reex  7945  cnelprrecn  7947  pnfnre  7999  mnfnre  8000  pnfxr  8010  nnex  8925  zex  9262  qex  9632  addex  9651  mulex  9652  ovshftex  10828  cnfldstr  13460  cnfldbas  13462  cnfldcj  13465  lmfval  13695  lmbrf  13718  lmfss  13747  lmres  13751  lmtopcnp  13753  cnmet  14033  cncfval  14062  elcncf  14063  limcrcl  14130  limccl  14131  ellimc3apf  14132  limccnp2lem  14148  limccnp2cntop  14149  reldvg  14151  dvfvalap  14153  dvbss  14157  dvidlemap  14163  dvcnp2cntop  14166  dvaddxxbr  14168  dvmulxxbr  14169  dvaddxx  14170  dvmulxx  14171  dviaddf  14172  dvimulf  14173  dvcoapbr  14174  dvcjbr  14175  dvcj  14176  dvfre  14177  dvexp  14178  dvrecap  14180  dvmptclx  14183  dvef  14191
  Copyright terms: Public domain W3C validator