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  7998  mnfnre  7999  pnfxr  8009  nnex  8924  zex  9261  qex  9631  addex  9650  mulex  9651  ovshftex  10827  cnfldstr  13427  cnfldbas  13429  cnfldcj  13432  lmfval  13662  lmbrf  13685  lmfss  13714  lmres  13718  lmtopcnp  13720  cnmet  14000  cncfval  14029  elcncf  14030  limcrcl  14097  limccl  14098  ellimc3apf  14099  limccnp2lem  14115  limccnp2cntop  14116  reldvg  14118  dvfvalap  14120  dvbss  14124  dvidlemap  14130  dvcnp2cntop  14133  dvaddxxbr  14135  dvmulxxbr  14136  dvaddxx  14137  dvmulxx  14138  dviaddf  14139  dvimulf  14140  dvcoapbr  14141  dvcjbr  14142  dvcj  14143  dvfre  14144  dvexp  14145  dvrecap  14147  dvmptclx  14150  dvef  14158
  Copyright terms: Public domain W3C validator