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

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

Proof of Theorem cnex
StepHypRef Expression
1 ax-cnex 7679 1 ℂ ∈ V
Colors of variables: wff set class
Syntax hints:  wcel 1465  Vcvv 2660  cc 7586
This theorem was proved from axioms:  ax-cnex 7679
This theorem is referenced by:  reex  7722  cnelprrecn  7724  pnfnre  7775  mnfnre  7776  pnfxr  7786  nnex  8694  zex  9031  qex  9392  ovshftex  10559  lmfval  12288  lmbrf  12311  lmfss  12340  lmres  12344  lmtopcnp  12346  cnmet  12626  cncfval  12655  elcncf  12656  limcrcl  12723  limccl  12724  ellimc3apf  12725  limccnp2lem  12741  limccnp2cntop  12742  reldvg  12744  dvfvalap  12746  dvbss  12750  dvidlemap  12756  dvcnp2cntop  12759  dvaddxxbr  12761  dvmulxxbr  12762  dvaddxx  12763  dvmulxx  12764  dviaddf  12765  dvimulf  12766  dvcoapbr  12767  dvcjbr  12768  dvcj  12769  dvfre  12770  dvexp  12771  dvrecap  12773  dvmptclx  12776  dvef  12783
  Copyright terms: Public domain W3C validator