| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > cnex | GIF version | ||
| Description: Alias for ax-cnex 8166. (Contributed by Mario Carneiro, 17-Nov-2014.) |
| Ref | Expression |
|---|---|
| cnex | ⊢ ℂ ∈ V |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-cnex 8166 | 1 ⊢ ℂ ∈ V |
| Colors of variables: wff set class |
| Syntax hints: ∈ wcel 2202 Vcvv 2803 ℂcc 8073 |
| This theorem was proved from axioms: ax-cnex 8166 |
| This theorem is referenced by: reex 8209 cnelprrecn 8211 pnfnre 8263 mnfnre 8264 pnfxr 8274 nnex 9191 zex 9532 qex 9910 addex 9930 mulex 9931 ovshftex 11442 cndsex 14632 cnfldstr 14637 cnfldbas 14639 mpocnfldadd 14640 mpocnfldmul 14642 cnfldcj 14644 expghmap 14686 lmfval 14987 lmbrf 15009 lmfss 15038 lmres 15042 lmtopcnp 15044 cnmet 15324 cncfval 15366 elcncf 15367 limcrcl 15452 limccl 15453 ellimc3apf 15454 limccnp2lem 15470 limccnp2cntop 15471 reldvg 15473 dvfvalap 15475 dvbss 15479 dvidlemap 15485 dvidrelem 15486 dvidsslem 15487 dvcnp2cntop 15493 dvaddxxbr 15495 dvmulxxbr 15496 dvaddxx 15497 dvmulxx 15498 dviaddf 15499 dvimulf 15500 dvcoapbr 15501 dvcjbr 15502 dvcj 15503 dvfre 15504 dvexp 15505 dvrecap 15507 dvmptclx 15512 dvef 15521 plyval 15526 elply 15528 elply2 15529 plyf 15531 plyss 15532 elplyr 15534 plyaddlem1 15541 plymullem1 15542 plyaddlem 15543 plymullem 15544 plysub 15547 plycolemc 15552 plyco 15553 plycj 15555 |
| Copyright terms: Public domain | W3C validator |