| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > cnex | GIF version | ||
| Description: Alias for ax-cnex 8113. (Contributed by Mario Carneiro, 17-Nov-2014.) |
| Ref | Expression |
|---|---|
| cnex | ⊢ ℂ ∈ V |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-cnex 8113 | 1 ⊢ ℂ ∈ V |
| Colors of variables: wff set class |
| Syntax hints: ∈ wcel 2200 Vcvv 2800 ℂcc 8020 |
| This theorem was proved from axioms: ax-cnex 8113 |
| This theorem is referenced by: reex 8156 cnelprrecn 8158 pnfnre 8211 mnfnre 8212 pnfxr 8222 nnex 9139 zex 9478 qex 9856 addex 9876 mulex 9877 ovshftex 11370 cndsex 14557 cnfldstr 14562 cnfldbas 14564 mpocnfldadd 14565 mpocnfldmul 14567 cnfldcj 14569 expghmap 14611 lmfval 14907 lmbrf 14929 lmfss 14958 lmres 14962 lmtopcnp 14964 cnmet 15244 cncfval 15286 elcncf 15287 limcrcl 15372 limccl 15373 ellimc3apf 15374 limccnp2lem 15390 limccnp2cntop 15391 reldvg 15393 dvfvalap 15395 dvbss 15399 dvidlemap 15405 dvidrelem 15406 dvidsslem 15407 dvcnp2cntop 15413 dvaddxxbr 15415 dvmulxxbr 15416 dvaddxx 15417 dvmulxx 15418 dviaddf 15419 dvimulf 15420 dvcoapbr 15421 dvcjbr 15422 dvcj 15423 dvfre 15424 dvexp 15425 dvrecap 15427 dvmptclx 15432 dvef 15441 plyval 15446 elply 15448 elply2 15449 plyf 15451 plyss 15452 elplyr 15454 plyaddlem1 15461 plymullem1 15462 plyaddlem 15463 plymullem 15464 plysub 15467 plycolemc 15472 plyco 15473 plycj 15475 |
| Copyright terms: Public domain | W3C validator |