| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > cnex | GIF version | ||
| Description: Alias for ax-cnex 8101. (Contributed by Mario Carneiro, 17-Nov-2014.) |
| Ref | Expression |
|---|---|
| cnex | ⊢ ℂ ∈ V |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-cnex 8101 | 1 ⊢ ℂ ∈ V |
| Colors of variables: wff set class |
| Syntax hints: ∈ wcel 2200 Vcvv 2799 ℂcc 8008 |
| This theorem was proved from axioms: ax-cnex 8101 |
| This theorem is referenced by: reex 8144 cnelprrecn 8146 pnfnre 8199 mnfnre 8200 pnfxr 8210 nnex 9127 zex 9466 qex 9839 addex 9859 mulex 9860 ovshftex 11345 cndsex 14532 cnfldstr 14537 cnfldbas 14539 mpocnfldadd 14540 mpocnfldmul 14542 cnfldcj 14544 expghmap 14586 lmfval 14882 lmbrf 14904 lmfss 14933 lmres 14937 lmtopcnp 14939 cnmet 15219 cncfval 15261 elcncf 15262 limcrcl 15347 limccl 15348 ellimc3apf 15349 limccnp2lem 15365 limccnp2cntop 15366 reldvg 15368 dvfvalap 15370 dvbss 15374 dvidlemap 15380 dvidrelem 15381 dvidsslem 15382 dvcnp2cntop 15388 dvaddxxbr 15390 dvmulxxbr 15391 dvaddxx 15392 dvmulxx 15393 dviaddf 15394 dvimulf 15395 dvcoapbr 15396 dvcjbr 15397 dvcj 15398 dvfre 15399 dvexp 15400 dvrecap 15402 dvmptclx 15407 dvef 15416 plyval 15421 elply 15423 elply2 15424 plyf 15426 plyss 15427 elplyr 15429 plyaddlem1 15436 plymullem1 15437 plyaddlem 15438 plymullem 15439 plysub 15442 plycolemc 15447 plyco 15448 plycj 15450 |
| Copyright terms: Public domain | W3C validator |