| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > cnex | GIF version | ||
| Description: Alias for ax-cnex 7973. (Contributed by Mario Carneiro, 17-Nov-2014.) |
| Ref | Expression |
|---|---|
| cnex | ⊢ ℂ ∈ V |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-cnex 7973 | 1 ⊢ ℂ ∈ V |
| Colors of variables: wff set class |
| Syntax hints: ∈ wcel 2167 Vcvv 2763 ℂcc 7880 |
| This theorem was proved from axioms: ax-cnex 7973 |
| This theorem is referenced by: reex 8016 cnelprrecn 8018 pnfnre 8071 mnfnre 8072 pnfxr 8082 nnex 8999 zex 9338 qex 9709 addex 9729 mulex 9730 ovshftex 10987 cndsex 14135 cnfldstr 14140 cnfldbas 14142 mpocnfldadd 14143 mpocnfldmul 14145 cnfldcj 14147 expghmap 14189 lmfval 14454 lmbrf 14477 lmfss 14506 lmres 14510 lmtopcnp 14512 cnmet 14792 cncfval 14834 elcncf 14835 limcrcl 14920 limccl 14921 ellimc3apf 14922 limccnp2lem 14938 limccnp2cntop 14939 reldvg 14941 dvfvalap 14943 dvbss 14947 dvidlemap 14953 dvidrelem 14954 dvidsslem 14955 dvcnp2cntop 14961 dvaddxxbr 14963 dvmulxxbr 14964 dvaddxx 14965 dvmulxx 14966 dviaddf 14967 dvimulf 14968 dvcoapbr 14969 dvcjbr 14970 dvcj 14971 dvfre 14972 dvexp 14973 dvrecap 14975 dvmptclx 14980 dvef 14989 plyval 14994 elply 14996 elply2 14997 plyf 14999 plyss 15000 elplyr 15002 plyaddlem1 15009 plymullem1 15010 plyaddlem 15011 plymullem 15012 plysub 15015 plycolemc 15020 plyco 15021 plycj 15023 |
| Copyright terms: Public domain | W3C validator |