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

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

Proof of Theorem cnex
StepHypRef Expression
1 ax-cnex 7904 1 ℂ ∈ V
Colors of variables: wff set class
Syntax hints:  wcel 2148  Vcvv 2739  cc 7811
This theorem was proved from axioms:  ax-cnex 7904
This theorem is referenced by:  reex  7947  cnelprrecn  7949  pnfnre  8001  mnfnre  8002  pnfxr  8012  nnex  8927  zex  9264  qex  9634  addex  9653  mulex  9654  ovshftex  10830  cnfldstr  13542  cnfldbas  13544  cnfldcj  13547  lmfval  13777  lmbrf  13800  lmfss  13829  lmres  13833  lmtopcnp  13835  cnmet  14115  cncfval  14144  elcncf  14145  limcrcl  14212  limccl  14213  ellimc3apf  14214  limccnp2lem  14230  limccnp2cntop  14231  reldvg  14233  dvfvalap  14235  dvbss  14239  dvidlemap  14245  dvcnp2cntop  14248  dvaddxxbr  14250  dvmulxxbr  14251  dvaddxx  14252  dvmulxx  14253  dviaddf  14254  dvimulf  14255  dvcoapbr  14256  dvcjbr  14257  dvcj  14258  dvfre  14259  dvexp  14260  dvrecap  14262  dvmptclx  14265  dvef  14273
  Copyright terms: Public domain W3C validator