![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > cnex | GIF version |
Description: Alias for ax-cnex 7916. (Contributed by Mario Carneiro, 17-Nov-2014.) |
Ref | Expression |
---|---|
cnex | ⊢ ℂ ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-cnex 7916 | 1 ⊢ ℂ ∈ V |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 2158 Vcvv 2749 ℂcc 7823 |
This theorem was proved from axioms: ax-cnex 7916 |
This theorem is referenced by: reex 7959 cnelprrecn 7961 pnfnre 8013 mnfnre 8014 pnfxr 8024 nnex 8939 zex 9276 qex 9646 addex 9665 mulex 9666 ovshftex 10842 cnfldstr 13739 cnfldbas 13741 cnfldcj 13744 lmfval 13988 lmbrf 14011 lmfss 14040 lmres 14044 lmtopcnp 14046 cnmet 14326 cncfval 14355 elcncf 14356 limcrcl 14423 limccl 14424 ellimc3apf 14425 limccnp2lem 14441 limccnp2cntop 14442 reldvg 14444 dvfvalap 14446 dvbss 14450 dvidlemap 14456 dvcnp2cntop 14459 dvaddxxbr 14461 dvmulxxbr 14462 dvaddxx 14463 dvmulxx 14464 dviaddf 14465 dvimulf 14466 dvcoapbr 14467 dvcjbr 14468 dvcj 14469 dvfre 14470 dvexp 14471 dvrecap 14473 dvmptclx 14476 dvef 14484 |
Copyright terms: Public domain | W3C validator |