![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > cnex | GIF version |
Description: Alias for ax-cnex 7963. (Contributed by Mario Carneiro, 17-Nov-2014.) |
Ref | Expression |
---|---|
cnex | ⊢ ℂ ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-cnex 7963 | 1 ⊢ ℂ ∈ V |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 2164 Vcvv 2760 ℂcc 7870 |
This theorem was proved from axioms: ax-cnex 7963 |
This theorem is referenced by: reex 8006 cnelprrecn 8008 pnfnre 8061 mnfnre 8062 pnfxr 8072 nnex 8988 zex 9326 qex 9697 addex 9717 mulex 9718 ovshftex 10963 cnfldstr 14049 cnfldbas 14051 cnfldcj 14056 expghmap 14095 lmfval 14360 lmbrf 14383 lmfss 14412 lmres 14416 lmtopcnp 14418 cnmet 14698 cncfval 14727 elcncf 14728 limcrcl 14812 limccl 14813 ellimc3apf 14814 limccnp2lem 14830 limccnp2cntop 14831 reldvg 14833 dvfvalap 14835 dvbss 14839 dvidlemap 14845 dvcnp2cntop 14848 dvaddxxbr 14850 dvmulxxbr 14851 dvaddxx 14852 dvmulxx 14853 dviaddf 14854 dvimulf 14855 dvcoapbr 14856 dvcjbr 14857 dvcj 14858 dvfre 14859 dvexp 14860 dvrecap 14862 dvmptclx 14865 dvef 14873 plyval 14878 elply 14880 elply2 14881 plyf 14883 plyss 14884 elplyr 14886 plyaddlem1 14893 plymullem1 14894 plyaddlem 14895 plymullem 14896 plysub 14899 |
Copyright terms: Public domain | W3C validator |