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

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

Proof of Theorem cnex
StepHypRef Expression
1 ax-cnex 8113 1 ℂ ∈ V
Colors of variables: wff set class
Syntax hints:  wcel 2200  Vcvv 2800  cc 8020
This theorem was proved from axioms:  ax-cnex 8113
This theorem is referenced by:  reex  8156  cnelprrecn  8158  pnfnre  8211  mnfnre  8212  pnfxr  8222  nnex  9139  zex  9478  qex  9856  addex  9876  mulex  9877  ovshftex  11370  cndsex  14557  cnfldstr  14562  cnfldbas  14564  mpocnfldadd  14565  mpocnfldmul  14567  cnfldcj  14569  expghmap  14611  lmfval  14907  lmbrf  14929  lmfss  14958  lmres  14962  lmtopcnp  14964  cnmet  15244  cncfval  15286  elcncf  15287  limcrcl  15372  limccl  15373  ellimc3apf  15374  limccnp2lem  15390  limccnp2cntop  15391  reldvg  15393  dvfvalap  15395  dvbss  15399  dvidlemap  15405  dvidrelem  15406  dvidsslem  15407  dvcnp2cntop  15413  dvaddxxbr  15415  dvmulxxbr  15416  dvaddxx  15417  dvmulxx  15418  dviaddf  15419  dvimulf  15420  dvcoapbr  15421  dvcjbr  15422  dvcj  15423  dvfre  15424  dvexp  15425  dvrecap  15427  dvmptclx  15432  dvef  15441  plyval  15446  elply  15448  elply2  15449  plyf  15451  plyss  15452  elplyr  15454  plyaddlem1  15461  plymullem1  15462  plyaddlem  15463  plymullem  15464  plysub  15467  plycolemc  15472  plyco  15473  plycj  15475
  Copyright terms: Public domain W3C validator