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

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

Proof of Theorem cnex
StepHypRef Expression
1 ax-cnex 7965 1  |-  CC  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 2164   _Vcvv 2760   CCcc 7872
This theorem was proved from axioms:  ax-cnex 7965
This theorem is referenced by:  reex  8008  cnelprrecn  8010  pnfnre  8063  mnfnre  8064  pnfxr  8074  nnex  8990  zex  9329  qex  9700  addex  9720  mulex  9721  ovshftex  10966  cndsex  14052  cnfldstr  14057  cnfldbas  14059  mpocnfldadd  14060  mpocnfldmul  14062  cnfldcj  14064  expghmap  14106  lmfval  14371  lmbrf  14394  lmfss  14423  lmres  14427  lmtopcnp  14429  cnmet  14709  cncfval  14751  elcncf  14752  limcrcl  14837  limccl  14838  ellimc3apf  14839  limccnp2lem  14855  limccnp2cntop  14856  reldvg  14858  dvfvalap  14860  dvbss  14864  dvidlemap  14870  dvidrelem  14871  dvidsslem  14872  dvcnp2cntop  14878  dvaddxxbr  14880  dvmulxxbr  14881  dvaddxx  14882  dvmulxx  14883  dviaddf  14884  dvimulf  14885  dvcoapbr  14886  dvcjbr  14887  dvcj  14888  dvfre  14889  dvexp  14890  dvrecap  14892  dvmptclx  14897  dvef  14906  plyval  14911  elply  14913  elply2  14914  plyf  14916  plyss  14917  elplyr  14919  plyaddlem1  14926  plymullem1  14927  plyaddlem  14928  plymullem  14929  plysub  14932  plycolemc  14936  plyco  14937  plycj  14939
  Copyright terms: Public domain W3C validator