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

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

Proof of Theorem cnex
StepHypRef Expression
1 ax-cnex 8086 1 ℂ ∈ V
Colors of variables: wff set class
Syntax hints:  wcel 2200  Vcvv 2799  cc 7993
This theorem was proved from axioms:  ax-cnex 8086
This theorem is referenced by:  reex  8129  cnelprrecn  8131  pnfnre  8184  mnfnre  8185  pnfxr  8195  nnex  9112  zex  9451  qex  9823  addex  9843  mulex  9844  ovshftex  11325  cndsex  14511  cnfldstr  14516  cnfldbas  14518  mpocnfldadd  14519  mpocnfldmul  14521  cnfldcj  14523  expghmap  14565  lmfval  14860  lmbrf  14883  lmfss  14912  lmres  14916  lmtopcnp  14918  cnmet  15198  cncfval  15240  elcncf  15241  limcrcl  15326  limccl  15327  ellimc3apf  15328  limccnp2lem  15344  limccnp2cntop  15345  reldvg  15347  dvfvalap  15349  dvbss  15353  dvidlemap  15359  dvidrelem  15360  dvidsslem  15361  dvcnp2cntop  15367  dvaddxxbr  15369  dvmulxxbr  15370  dvaddxx  15371  dvmulxx  15372  dviaddf  15373  dvimulf  15374  dvcoapbr  15375  dvcjbr  15376  dvcj  15377  dvfre  15378  dvexp  15379  dvrecap  15381  dvmptclx  15386  dvef  15395  plyval  15400  elply  15402  elply2  15403  plyf  15405  plyss  15406  elplyr  15408  plyaddlem1  15415  plymullem1  15416  plyaddlem  15417  plymullem  15418  plysub  15421  plycolemc  15426  plyco  15427  plycj  15429
  Copyright terms: Public domain W3C validator