| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > cnex | GIF version | ||
| Description: Alias for ax-cnex 8086. (Contributed by Mario Carneiro, 17-Nov-2014.) |
| Ref | Expression |
|---|---|
| cnex | ⊢ ℂ ∈ V |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-cnex 8086 | 1 ⊢ ℂ ∈ V |
| Colors of variables: wff set class |
| Syntax hints: ∈ wcel 2200 Vcvv 2799 ℂcc 7993 |
| This theorem was proved from axioms: ax-cnex 8086 |
| This theorem is referenced by: reex 8129 cnelprrecn 8131 pnfnre 8184 mnfnre 8185 pnfxr 8195 nnex 9112 zex 9451 qex 9823 addex 9843 mulex 9844 ovshftex 11325 cndsex 14511 cnfldstr 14516 cnfldbas 14518 mpocnfldadd 14519 mpocnfldmul 14521 cnfldcj 14523 expghmap 14565 lmfval 14860 lmbrf 14883 lmfss 14912 lmres 14916 lmtopcnp 14918 cnmet 15198 cncfval 15240 elcncf 15241 limcrcl 15326 limccl 15327 ellimc3apf 15328 limccnp2lem 15344 limccnp2cntop 15345 reldvg 15347 dvfvalap 15349 dvbss 15353 dvidlemap 15359 dvidrelem 15360 dvidsslem 15361 dvcnp2cntop 15367 dvaddxxbr 15369 dvmulxxbr 15370 dvaddxx 15371 dvmulxx 15372 dviaddf 15373 dvimulf 15374 dvcoapbr 15375 dvcjbr 15376 dvcj 15377 dvfre 15378 dvexp 15379 dvrecap 15381 dvmptclx 15386 dvef 15395 plyval 15400 elply 15402 elply2 15403 plyf 15405 plyss 15406 elplyr 15408 plyaddlem1 15415 plymullem1 15416 plyaddlem 15417 plymullem 15418 plysub 15421 plycolemc 15426 plyco 15427 plycj 15429 |
| Copyright terms: Public domain | W3C validator |