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

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

Proof of Theorem cnex
StepHypRef Expression
1 ax-cnex 7963 1 ℂ ∈ V
Colors of variables: wff set class
Syntax hints:  wcel 2164  Vcvv 2760  cc 7870
This theorem was proved from axioms:  ax-cnex 7963
This theorem is referenced by:  reex  8006  cnelprrecn  8008  pnfnre  8061  mnfnre  8062  pnfxr  8072  nnex  8988  zex  9326  qex  9697  addex  9717  mulex  9718  ovshftex  10963  cnfldstr  14049  cnfldbas  14051  cnfldcj  14056  expghmap  14095  lmfval  14360  lmbrf  14383  lmfss  14412  lmres  14416  lmtopcnp  14418  cnmet  14698  cncfval  14727  elcncf  14728  limcrcl  14812  limccl  14813  ellimc3apf  14814  limccnp2lem  14830  limccnp2cntop  14831  reldvg  14833  dvfvalap  14835  dvbss  14839  dvidlemap  14845  dvcnp2cntop  14848  dvaddxxbr  14850  dvmulxxbr  14851  dvaddxx  14852  dvmulxx  14853  dviaddf  14854  dvimulf  14855  dvcoapbr  14856  dvcjbr  14857  dvcj  14858  dvfre  14859  dvexp  14860  dvrecap  14862  dvmptclx  14865  dvef  14873  plyval  14878  elply  14880  elply2  14881  plyf  14883  plyss  14884  elplyr  14886  plyaddlem1  14893  plymullem1  14894  plyaddlem  14895  plymullem  14896  plysub  14899
  Copyright terms: Public domain W3C validator