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

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

Proof of Theorem cnex
StepHypRef Expression
1 ax-cnex 8271 1 ℂ ∈ V
Colors of variables:    wff set class
This proof depends on syntax axioms:   ∈ wcel 2209  Vcvv 2821  ℂcc 8178
This proof depends on axioms:  ax-cnex 8271
This theorem is used by:  reex  8314  cnelprrecn  8316  pnfnre  8368  mnfnre  8369  pnfxr  8379  nnex  9313  zex  9658  qex  10042  addex  10063  mulex  10064  ovshftex  11600  cndsex  14974  cnfldstr  14979  cnfldbas  14981  mpocnfldadd  14982  mpocnfldmul  14984  cnfldcj  14986  expghmap  15026  lmfval  15385  lmbrf  15407  lmfss  15436  lmres  15440  lmtopcnp  15442  cnmet  15722  cncfval  15764  elcncf  15765  limcrcl  15850  limccl  15851  ellimc3apf  15852  limccnp2lem  15868  limccnp2cntop  15869  reldvg  15871  dvfvalap  15873  dvbss  15877  dvidlemap  15883  dvidrelem  15884  dvidsslem  15885  dvcnp2cntop  15891  dvaddxxbr  15893  dvmulxxbr  15894  dvaddxx  15895  dvmulxx  15896  dviaddf  15897  dvimulf  15898  dvcoapbr  15899  dvcjbr  15900  dvcj  15901  dvfre  15902  dvexp  15903  dvrecap  15905  dvmptclx  15910  dvef  15919  plyval  15924  elply  15926  elply2  15927  plyf  15929  plyss  15930  elplyr  15932  plyaddlem1  15939  plymullem1  15940  plyaddlem  15941  plymullem  15942  plysub  15945  plycolemc  15950  plyco  15951  plycj  15953
  Copyright terms: Public domain W3C validator