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

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

Proof of Theorem cnex
StepHypRef Expression
1 ax-cnex 8123 1  |-  CC  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 2202   _Vcvv 2802   CCcc 8030
This theorem was proved from axioms:  ax-cnex 8123
This theorem is referenced by:  reex  8166  cnelprrecn  8168  pnfnre  8221  mnfnre  8222  pnfxr  8232  nnex  9149  zex  9488  qex  9866  addex  9886  mulex  9887  ovshftex  11397  cndsex  14586  cnfldstr  14591  cnfldbas  14593  mpocnfldadd  14594  mpocnfldmul  14596  cnfldcj  14598  expghmap  14640  lmfval  14936  lmbrf  14958  lmfss  14987  lmres  14991  lmtopcnp  14993  cnmet  15273  cncfval  15315  elcncf  15316  limcrcl  15401  limccl  15402  ellimc3apf  15403  limccnp2lem  15419  limccnp2cntop  15420  reldvg  15422  dvfvalap  15424  dvbss  15428  dvidlemap  15434  dvidrelem  15435  dvidsslem  15436  dvcnp2cntop  15442  dvaddxxbr  15444  dvmulxxbr  15445  dvaddxx  15446  dvmulxx  15447  dviaddf  15448  dvimulf  15449  dvcoapbr  15450  dvcjbr  15451  dvcj  15452  dvfre  15453  dvexp  15454  dvrecap  15456  dvmptclx  15461  dvef  15470  plyval  15475  elply  15477  elply2  15478  plyf  15480  plyss  15481  elplyr  15483  plyaddlem1  15490  plymullem1  15491  plyaddlem  15492  plymullem  15493  plysub  15496  plycolemc  15501  plyco  15502  plycj  15504
  Copyright terms: Public domain W3C validator