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

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

Proof of Theorem cnex
StepHypRef Expression
1 ax-cnex 8018 1  |-  CC  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 2176   _Vcvv 2772   CCcc 7925
This theorem was proved from axioms:  ax-cnex 8018
This theorem is referenced by:  reex  8061  cnelprrecn  8063  pnfnre  8116  mnfnre  8117  pnfxr  8127  nnex  9044  zex  9383  qex  9755  addex  9775  mulex  9776  ovshftex  11163  cndsex  14348  cnfldstr  14353  cnfldbas  14355  mpocnfldadd  14356  mpocnfldmul  14358  cnfldcj  14360  expghmap  14402  lmfval  14697  lmbrf  14720  lmfss  14749  lmres  14753  lmtopcnp  14755  cnmet  15035  cncfval  15077  elcncf  15078  limcrcl  15163  limccl  15164  ellimc3apf  15165  limccnp2lem  15181  limccnp2cntop  15182  reldvg  15184  dvfvalap  15186  dvbss  15190  dvidlemap  15196  dvidrelem  15197  dvidsslem  15198  dvcnp2cntop  15204  dvaddxxbr  15206  dvmulxxbr  15207  dvaddxx  15208  dvmulxx  15209  dviaddf  15210  dvimulf  15211  dvcoapbr  15212  dvcjbr  15213  dvcj  15214  dvfre  15215  dvexp  15216  dvrecap  15218  dvmptclx  15223  dvef  15232  plyval  15237  elply  15239  elply2  15240  plyf  15242  plyss  15243  elplyr  15245  plyaddlem1  15252  plymullem1  15253  plyaddlem  15254  plymullem  15255  plysub  15258  plycolemc  15263  plyco  15264  plycj  15266
  Copyright terms: Public domain W3C validator