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

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

Proof of Theorem cnex
StepHypRef Expression
1 ax-cnex 7916 1 ℂ ∈ V
Colors of variables: wff set class
Syntax hints:  wcel 2158  Vcvv 2749  cc 7823
This theorem was proved from axioms:  ax-cnex 7916
This theorem is referenced by:  reex  7959  cnelprrecn  7961  pnfnre  8013  mnfnre  8014  pnfxr  8024  nnex  8939  zex  9276  qex  9646  addex  9665  mulex  9666  ovshftex  10842  cnfldstr  13739  cnfldbas  13741  cnfldcj  13744  lmfval  13988  lmbrf  14011  lmfss  14040  lmres  14044  lmtopcnp  14046  cnmet  14326  cncfval  14355  elcncf  14356  limcrcl  14423  limccl  14424  ellimc3apf  14425  limccnp2lem  14441  limccnp2cntop  14442  reldvg  14444  dvfvalap  14446  dvbss  14450  dvidlemap  14456  dvcnp2cntop  14459  dvaddxxbr  14461  dvmulxxbr  14462  dvaddxx  14463  dvmulxx  14464  dviaddf  14465  dvimulf  14466  dvcoapbr  14467  dvcjbr  14468  dvcj  14469  dvfre  14470  dvexp  14471  dvrecap  14473  dvmptclx  14476  dvef  14484
  Copyright terms: Public domain W3C validator