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

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

Proof of Theorem cnex
StepHypRef Expression
1 ax-cnex 7118 1 ℂ ∈ V
Colors of variables: wff set class
Syntax hints:  wcel 1434  Vcvv 2602  cc 7030
This theorem was proved from axioms:  ax-cnex 7118
This theorem is referenced by:  reex  7158  cnelprrecn  7160  pnfnre  7211  mnfnre  7212  pnfxr  7222  nnex  8101  zex  8430  qex  8787  iseradd  9548  isersub  9549  serige0  9559  serile  9560  ibcval5  9776  ovshftex  9834  clim2iser  10302  clim2iser2  10303  iisermulc2  10305  iserile  10307  climserile  10310  fisumcvg  10327
  Copyright terms: Public domain W3C validator