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

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

Proof of Theorem cnex
StepHypRef Expression
1 ax-cnex 8051 1  |-  CC  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 2178   _Vcvv 2776   CCcc 7958
This theorem was proved from axioms:  ax-cnex 8051
This theorem is referenced by:  reex  8094  cnelprrecn  8096  pnfnre  8149  mnfnre  8150  pnfxr  8160  nnex  9077  zex  9416  qex  9788  addex  9808  mulex  9809  ovshftex  11245  cndsex  14430  cnfldstr  14435  cnfldbas  14437  mpocnfldadd  14438  mpocnfldmul  14440  cnfldcj  14442  expghmap  14484  lmfval  14779  lmbrf  14802  lmfss  14831  lmres  14835  lmtopcnp  14837  cnmet  15117  cncfval  15159  elcncf  15160  limcrcl  15245  limccl  15246  ellimc3apf  15247  limccnp2lem  15263  limccnp2cntop  15264  reldvg  15266  dvfvalap  15268  dvbss  15272  dvidlemap  15278  dvidrelem  15279  dvidsslem  15280  dvcnp2cntop  15286  dvaddxxbr  15288  dvmulxxbr  15289  dvaddxx  15290  dvmulxx  15291  dviaddf  15292  dvimulf  15293  dvcoapbr  15294  dvcjbr  15295  dvcj  15296  dvfre  15297  dvexp  15298  dvrecap  15300  dvmptclx  15305  dvef  15314  plyval  15319  elply  15321  elply2  15322  plyf  15324  plyss  15325  elplyr  15327  plyaddlem1  15334  plymullem1  15335  plyaddlem  15336  plymullem  15337  plysub  15340  plycolemc  15345  plyco  15346  plycj  15348
  Copyright terms: Public domain W3C validator