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

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

Proof of Theorem cnex
StepHypRef Expression
1 ax-cnex 8016 1  |-  CC  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 2176   _Vcvv 2772   CCcc 7923
This theorem was proved from axioms:  ax-cnex 8016
This theorem is referenced by:  reex  8059  cnelprrecn  8061  pnfnre  8114  mnfnre  8115  pnfxr  8125  nnex  9042  zex  9381  qex  9753  addex  9773  mulex  9774  ovshftex  11130  cndsex  14315  cnfldstr  14320  cnfldbas  14322  mpocnfldadd  14323  mpocnfldmul  14325  cnfldcj  14327  expghmap  14369  lmfval  14664  lmbrf  14687  lmfss  14716  lmres  14720  lmtopcnp  14722  cnmet  15002  cncfval  15044  elcncf  15045  limcrcl  15130  limccl  15131  ellimc3apf  15132  limccnp2lem  15148  limccnp2cntop  15149  reldvg  15151  dvfvalap  15153  dvbss  15157  dvidlemap  15163  dvidrelem  15164  dvidsslem  15165  dvcnp2cntop  15171  dvaddxxbr  15173  dvmulxxbr  15174  dvaddxx  15175  dvmulxx  15176  dviaddf  15177  dvimulf  15178  dvcoapbr  15179  dvcjbr  15180  dvcj  15181  dvfre  15182  dvexp  15183  dvrecap  15185  dvmptclx  15190  dvef  15199  plyval  15204  elply  15206  elply2  15207  plyf  15209  plyss  15210  elplyr  15212  plyaddlem1  15219  plymullem1  15220  plyaddlem  15221  plymullem  15222  plysub  15225  plycolemc  15230  plyco  15231  plycj  15233
  Copyright terms: Public domain W3C validator