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

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

Proof of Theorem cnex
StepHypRef Expression
1 ax-cnex 8183 1  |-  CC  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 2202   _Vcvv 2803   CCcc 8090
This theorem was proved from axioms:  ax-cnex 8183
This theorem is referenced by:  reex  8226  cnelprrecn  8228  pnfnre  8280  mnfnre  8281  pnfxr  8291  nnex  9208  zex  9549  qex  9927  addex  9947  mulex  9948  ovshftex  11459  cndsex  14649  cnfldstr  14654  cnfldbas  14656  mpocnfldadd  14657  mpocnfldmul  14659  cnfldcj  14661  expghmap  14703  lmfval  15004  lmbrf  15026  lmfss  15055  lmres  15059  lmtopcnp  15061  cnmet  15341  cncfval  15383  elcncf  15384  limcrcl  15469  limccl  15470  ellimc3apf  15471  limccnp2lem  15487  limccnp2cntop  15488  reldvg  15490  dvfvalap  15492  dvbss  15496  dvidlemap  15502  dvidrelem  15503  dvidsslem  15504  dvcnp2cntop  15510  dvaddxxbr  15512  dvmulxxbr  15513  dvaddxx  15514  dvmulxx  15515  dviaddf  15516  dvimulf  15517  dvcoapbr  15518  dvcjbr  15519  dvcj  15520  dvfre  15521  dvexp  15522  dvrecap  15524  dvmptclx  15529  dvef  15538  plyval  15543  elply  15545  elply2  15546  plyf  15548  plyss  15549  elplyr  15551  plyaddlem1  15558  plymullem1  15559  plyaddlem  15560  plymullem  15561  plysub  15564  plycolemc  15569  plyco  15570  plycj  15572
  Copyright terms: Public domain W3C validator