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

Theorem cnex 8156
Description: Alias for ax-cnex 8123. (Contributed by Mario Carneiro, 17-Nov-2014.)
Assertion
Ref Expression
cnex ℂ ∈ V

Proof of Theorem cnex
StepHypRef Expression
1 ax-cnex 8123 1 ℂ ∈ V
Colors of variables: wff set class
Syntax hints:  wcel 2202  Vcvv 2802  cc 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  11384  cndsex  14573  cnfldstr  14578  cnfldbas  14580  mpocnfldadd  14581  mpocnfldmul  14583  cnfldcj  14585  expghmap  14627  lmfval  14923  lmbrf  14945  lmfss  14974  lmres  14978  lmtopcnp  14980  cnmet  15260  cncfval  15302  elcncf  15303  limcrcl  15388  limccl  15389  ellimc3apf  15390  limccnp2lem  15406  limccnp2cntop  15407  reldvg  15409  dvfvalap  15411  dvbss  15415  dvidlemap  15421  dvidrelem  15422  dvidsslem  15423  dvcnp2cntop  15429  dvaddxxbr  15431  dvmulxxbr  15432  dvaddxx  15433  dvmulxx  15434  dviaddf  15435  dvimulf  15436  dvcoapbr  15437  dvcjbr  15438  dvcj  15439  dvfre  15440  dvexp  15441  dvrecap  15443  dvmptclx  15448  dvef  15457  plyval  15462  elply  15464  elply2  15465  plyf  15467  plyss  15468  elplyr  15470  plyaddlem1  15477  plymullem1  15478  plyaddlem  15479  plymullem  15480  plysub  15483  plycolemc  15488  plyco  15489  plycj  15491
  Copyright terms: Public domain W3C validator