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

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

Proof of Theorem cnex
StepHypRef Expression
1 ax-cnex 8031 1 ℂ ∈ V
Colors of variables: wff set class
Syntax hints:  wcel 2177  Vcvv 2773  cc 7938
This theorem was proved from axioms:  ax-cnex 8031
This theorem is referenced by:  reex  8074  cnelprrecn  8076  pnfnre  8129  mnfnre  8130  pnfxr  8140  nnex  9057  zex  9396  qex  9768  addex  9788  mulex  9789  ovshftex  11200  cndsex  14385  cnfldstr  14390  cnfldbas  14392  mpocnfldadd  14393  mpocnfldmul  14395  cnfldcj  14397  expghmap  14439  lmfval  14734  lmbrf  14757  lmfss  14786  lmres  14790  lmtopcnp  14792  cnmet  15072  cncfval  15114  elcncf  15115  limcrcl  15200  limccl  15201  ellimc3apf  15202  limccnp2lem  15218  limccnp2cntop  15219  reldvg  15221  dvfvalap  15223  dvbss  15227  dvidlemap  15233  dvidrelem  15234  dvidsslem  15235  dvcnp2cntop  15241  dvaddxxbr  15243  dvmulxxbr  15244  dvaddxx  15245  dvmulxx  15246  dviaddf  15247  dvimulf  15248  dvcoapbr  15249  dvcjbr  15250  dvcj  15251  dvfre  15252  dvexp  15253  dvrecap  15255  dvmptclx  15260  dvef  15269  plyval  15274  elply  15276  elply2  15277  plyf  15279  plyss  15280  elplyr  15282  plyaddlem1  15289  plymullem1  15290  plyaddlem  15291  plymullem  15292  plysub  15295  plycolemc  15300  plyco  15301  plycj  15303
  Copyright terms: Public domain W3C validator