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

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

Proof of Theorem cnex
StepHypRef Expression
1 ax-cnex 8122 1 ℂ ∈ V
Colors of variables: wff set class
Syntax hints:  wcel 2202  Vcvv 2802  cc 8029
This theorem was proved from axioms:  ax-cnex 8122
This theorem is referenced by:  reex  8165  cnelprrecn  8167  pnfnre  8220  mnfnre  8221  pnfxr  8231  nnex  9148  zex  9487  qex  9865  addex  9885  mulex  9886  ovshftex  11379  cndsex  14566  cnfldstr  14571  cnfldbas  14573  mpocnfldadd  14574  mpocnfldmul  14576  cnfldcj  14578  expghmap  14620  lmfval  14916  lmbrf  14938  lmfss  14967  lmres  14971  lmtopcnp  14973  cnmet  15253  cncfval  15295  elcncf  15296  limcrcl  15381  limccl  15382  ellimc3apf  15383  limccnp2lem  15399  limccnp2cntop  15400  reldvg  15402  dvfvalap  15404  dvbss  15408  dvidlemap  15414  dvidrelem  15415  dvidsslem  15416  dvcnp2cntop  15422  dvaddxxbr  15424  dvmulxxbr  15425  dvaddxx  15426  dvmulxx  15427  dviaddf  15428  dvimulf  15429  dvcoapbr  15430  dvcjbr  15431  dvcj  15432  dvfre  15433  dvexp  15434  dvrecap  15436  dvmptclx  15441  dvef  15450  plyval  15455  elply  15457  elply2  15458  plyf  15460  plyss  15461  elplyr  15463  plyaddlem1  15470  plymullem1  15471  plyaddlem  15472  plymullem  15473  plysub  15476  plycolemc  15481  plyco  15482  plycj  15484
  Copyright terms: Public domain W3C validator