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

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

Proof of Theorem cnex
StepHypRef Expression
1 ax-cnex 7897 1  |-  CC  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 2148   _Vcvv 2737   CCcc 7804
This theorem was proved from axioms:  ax-cnex 7897
This theorem is referenced by:  reex  7940  cnelprrecn  7942  pnfnre  7993  mnfnre  7994  pnfxr  8004  nnex  8919  zex  9256  qex  9626  addex  9645  mulex  9646  ovshftex  10819  cnfldstr  13262  cnfldbas  13264  cnfldcj  13267  lmfval  13474  lmbrf  13497  lmfss  13526  lmres  13530  lmtopcnp  13532  cnmet  13812  cncfval  13841  elcncf  13842  limcrcl  13909  limccl  13910  ellimc3apf  13911  limccnp2lem  13927  limccnp2cntop  13928  reldvg  13930  dvfvalap  13932  dvbss  13936  dvidlemap  13942  dvcnp2cntop  13945  dvaddxxbr  13947  dvmulxxbr  13948  dvaddxx  13949  dvmulxx  13950  dviaddf  13951  dvimulf  13952  dvcoapbr  13953  dvcjbr  13954  dvcj  13955  dvfre  13956  dvexp  13957  dvrecap  13959  dvmptclx  13962  dvef  13970
  Copyright terms: Public domain W3C validator