| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > cnex | GIF version | ||
| Description: Alias for ax-cnex 8122. (Contributed by Mario Carneiro, 17-Nov-2014.) |
| Ref | Expression |
|---|---|
| cnex | ⊢ ℂ ∈ V |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-cnex 8122 | 1 ⊢ ℂ ∈ V |
| Colors of variables: wff set class |
| Syntax hints: ∈ wcel 2202 Vcvv 2802 ℂcc 8029 |
| This theorem was proved from axioms: ax-cnex 8122 |
| This theorem is referenced by: reex 8165 cnelprrecn 8167 pnfnre 8220 mnfnre 8221 pnfxr 8231 nnex 9148 zex 9487 qex 9865 addex 9885 mulex 9886 ovshftex 11379 cndsex 14566 cnfldstr 14571 cnfldbas 14573 mpocnfldadd 14574 mpocnfldmul 14576 cnfldcj 14578 expghmap 14620 lmfval 14916 lmbrf 14938 lmfss 14967 lmres 14971 lmtopcnp 14973 cnmet 15253 cncfval 15295 elcncf 15296 limcrcl 15381 limccl 15382 ellimc3apf 15383 limccnp2lem 15399 limccnp2cntop 15400 reldvg 15402 dvfvalap 15404 dvbss 15408 dvidlemap 15414 dvidrelem 15415 dvidsslem 15416 dvcnp2cntop 15422 dvaddxxbr 15424 dvmulxxbr 15425 dvaddxx 15426 dvmulxx 15427 dviaddf 15428 dvimulf 15429 dvcoapbr 15430 dvcjbr 15431 dvcj 15432 dvfre 15433 dvexp 15434 dvrecap 15436 dvmptclx 15441 dvef 15450 plyval 15455 elply 15457 elply2 15458 plyf 15460 plyss 15461 elplyr 15463 plyaddlem1 15470 plymullem1 15471 plyaddlem 15472 plymullem 15473 plysub 15476 plycolemc 15481 plyco 15482 plycj 15484 |
| Copyright terms: Public domain | W3C validator |