| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > cnex | GIF version | ||
| Description: Alias for ax-cnex 8123. (Contributed by Mario Carneiro, 17-Nov-2014.) |
| Ref | Expression |
|---|---|
| cnex | ⊢ ℂ ∈ V |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-cnex 8123 | 1 ⊢ ℂ ∈ V |
| Colors of variables: wff set class |
| Syntax hints: ∈ wcel 2202 Vcvv 2802 ℂcc 8030 |
| This theorem was proved from axioms: ax-cnex 8123 |
| This theorem is referenced by: reex 8166 cnelprrecn 8168 pnfnre 8221 mnfnre 8222 pnfxr 8232 nnex 9149 zex 9488 qex 9866 addex 9886 mulex 9887 ovshftex 11384 cndsex 14573 cnfldstr 14578 cnfldbas 14580 mpocnfldadd 14581 mpocnfldmul 14583 cnfldcj 14585 expghmap 14627 lmfval 14923 lmbrf 14945 lmfss 14974 lmres 14978 lmtopcnp 14980 cnmet 15260 cncfval 15302 elcncf 15303 limcrcl 15388 limccl 15389 ellimc3apf 15390 limccnp2lem 15406 limccnp2cntop 15407 reldvg 15409 dvfvalap 15411 dvbss 15415 dvidlemap 15421 dvidrelem 15422 dvidsslem 15423 dvcnp2cntop 15429 dvaddxxbr 15431 dvmulxxbr 15432 dvaddxx 15433 dvmulxx 15434 dviaddf 15435 dvimulf 15436 dvcoapbr 15437 dvcjbr 15438 dvcj 15439 dvfre 15440 dvexp 15441 dvrecap 15443 dvmptclx 15448 dvef 15457 plyval 15462 elply 15464 elply2 15465 plyf 15467 plyss 15468 elplyr 15470 plyaddlem1 15477 plymullem1 15478 plyaddlem 15479 plymullem 15480 plysub 15483 plycolemc 15488 plyco 15489 plycj 15491 |
| Copyright terms: Public domain | W3C validator |