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

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

Proof of Theorem cnex
StepHypRef Expression
1 ax-cnex 6973 1 ℂ ∈ V
Colors of variables: wff set class
Syntax hints:  wcel 1393  Vcvv 2557  cc 6885
This theorem was proved from axioms:  ax-cnex 6973
This theorem is referenced by:  reex  7013  cnelprrecn  7015  pnfnre  7065  mnfnre  7066  nnex  7918  zex  8252  qex  8565  pnfxr  8690  iserf  9207  iseradd  9217  isersub  9218  iser0  9224  iser0f  9225  serige0  9226  serile  9227  expivallem  9230  expival  9231  exp1  9235  expp1  9236  ovshftex  9394  clim2iser  9831  clim2iser2  9832  iisermulc2  9834  iserile  9836  climserile  9839  serif0  9845
  Copyright terms: Public domain W3C validator