| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > cnex | GIF version | ||
| Description: Alias for ax-cnex 7989. (Contributed by Mario Carneiro, 17-Nov-2014.) |
| Ref | Expression |
|---|---|
| cnex | ⊢ ℂ ∈ V |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-cnex 7989 | 1 ⊢ ℂ ∈ V |
| Colors of variables: wff set class |
| Syntax hints: ∈ wcel 2167 Vcvv 2763 ℂcc 7896 |
| This theorem was proved from axioms: ax-cnex 7989 |
| This theorem is referenced by: reex 8032 cnelprrecn 8034 pnfnre 8087 mnfnre 8088 pnfxr 8098 nnex 9015 zex 9354 qex 9725 addex 9745 mulex 9746 ovshftex 11003 cndsex 14187 cnfldstr 14192 cnfldbas 14194 mpocnfldadd 14195 mpocnfldmul 14197 cnfldcj 14199 expghmap 14241 lmfval 14536 lmbrf 14559 lmfss 14588 lmres 14592 lmtopcnp 14594 cnmet 14874 cncfval 14916 elcncf 14917 limcrcl 15002 limccl 15003 ellimc3apf 15004 limccnp2lem 15020 limccnp2cntop 15021 reldvg 15023 dvfvalap 15025 dvbss 15029 dvidlemap 15035 dvidrelem 15036 dvidsslem 15037 dvcnp2cntop 15043 dvaddxxbr 15045 dvmulxxbr 15046 dvaddxx 15047 dvmulxx 15048 dviaddf 15049 dvimulf 15050 dvcoapbr 15051 dvcjbr 15052 dvcj 15053 dvfre 15054 dvexp 15055 dvrecap 15057 dvmptclx 15062 dvef 15071 plyval 15076 elply 15078 elply2 15079 plyf 15081 plyss 15082 elplyr 15084 plyaddlem1 15091 plymullem1 15092 plyaddlem 15093 plymullem 15094 plysub 15097 plycolemc 15102 plyco 15103 plycj 15105 |
| Copyright terms: Public domain | W3C validator |