| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > cnex | GIF version | ||
| Description: Alias for ax-cnex 8031. (Contributed by Mario Carneiro, 17-Nov-2014.) |
| Ref | Expression |
|---|---|
| cnex | ⊢ ℂ ∈ V |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-cnex 8031 | 1 ⊢ ℂ ∈ V |
| Colors of variables: wff set class |
| Syntax hints: ∈ wcel 2177 Vcvv 2773 ℂcc 7938 |
| This theorem was proved from axioms: ax-cnex 8031 |
| This theorem is referenced by: reex 8074 cnelprrecn 8076 pnfnre 8129 mnfnre 8130 pnfxr 8140 nnex 9057 zex 9396 qex 9768 addex 9788 mulex 9789 ovshftex 11200 cndsex 14385 cnfldstr 14390 cnfldbas 14392 mpocnfldadd 14393 mpocnfldmul 14395 cnfldcj 14397 expghmap 14439 lmfval 14734 lmbrf 14757 lmfss 14786 lmres 14790 lmtopcnp 14792 cnmet 15072 cncfval 15114 elcncf 15115 limcrcl 15200 limccl 15201 ellimc3apf 15202 limccnp2lem 15218 limccnp2cntop 15219 reldvg 15221 dvfvalap 15223 dvbss 15227 dvidlemap 15233 dvidrelem 15234 dvidsslem 15235 dvcnp2cntop 15241 dvaddxxbr 15243 dvmulxxbr 15244 dvaddxx 15245 dvmulxx 15246 dviaddf 15247 dvimulf 15248 dvcoapbr 15249 dvcjbr 15250 dvcj 15251 dvfre 15252 dvexp 15253 dvrecap 15255 dvmptclx 15260 dvef 15269 plyval 15274 elply 15276 elply2 15277 plyf 15279 plyss 15280 elplyr 15282 plyaddlem1 15289 plymullem1 15290 plyaddlem 15291 plymullem 15292 plysub 15295 plycolemc 15300 plyco 15301 plycj 15303 |
| Copyright terms: Public domain | W3C validator |