![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > cnex | GIF version |
Description: Alias for ax-cnex 7118. (Contributed by Mario Carneiro, 17-Nov-2014.) |
Ref | Expression |
---|---|
cnex | ⊢ ℂ ∈ V |
Step | Hyp | Ref | 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 |