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

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

Proof of Theorem cnex
StepHypRef Expression
1 ax-cnex 8090 1  |-  CC  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 2200   _Vcvv 2799   CCcc 7997
This theorem was proved from axioms:  ax-cnex 8090
This theorem is referenced by:  reex  8133  cnelprrecn  8135  pnfnre  8188  mnfnre  8189  pnfxr  8199  nnex  9116  zex  9455  qex  9827  addex  9847  mulex  9848  ovshftex  11330  cndsex  14517  cnfldstr  14522  cnfldbas  14524  mpocnfldadd  14525  mpocnfldmul  14527  cnfldcj  14529  expghmap  14571  lmfval  14867  lmbrf  14889  lmfss  14918  lmres  14922  lmtopcnp  14924  cnmet  15204  cncfval  15246  elcncf  15247  limcrcl  15332  limccl  15333  ellimc3apf  15334  limccnp2lem  15350  limccnp2cntop  15351  reldvg  15353  dvfvalap  15355  dvbss  15359  dvidlemap  15365  dvidrelem  15366  dvidsslem  15367  dvcnp2cntop  15373  dvaddxxbr  15375  dvmulxxbr  15376  dvaddxx  15377  dvmulxx  15378  dviaddf  15379  dvimulf  15380  dvcoapbr  15381  dvcjbr  15382  dvcj  15383  dvfre  15384  dvexp  15385  dvrecap  15387  dvmptclx  15392  dvef  15401  plyval  15406  elply  15408  elply2  15409  plyf  15411  plyss  15412  elplyr  15414  plyaddlem1  15421  plymullem1  15422  plyaddlem  15423  plymullem  15424  plysub  15427  plycolemc  15432  plyco  15433  plycj  15435
  Copyright terms: Public domain W3C validator