| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > cnex | GIF version | ||
| Description: Alias for ax-cnex 8260. (Contributed by Mario Carneiro, 17-Nov-2014.) |
| Ref | Expression |
|---|---|
| cnex | ⊢ ℂ ∈ V |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-cnex 8260 | 1 ⊢ ℂ ∈ V |
| Colors of variables: wff set class |
| Syntax hints: ∈ wcel 2209 Vcvv 2821 ℂcc 8167 |
| This theorem was proved from axioms: ax-cnex 8260 |
| This theorem is referenced by: reex 8303 cnelprrecn 8305 pnfnre 8357 mnfnre 8358 pnfxr 8368 nnex 9289 zex 9632 qex 10011 addex 10031 mulex 10032 ovshftex 11562 cndsex 14862 cnfldstr 14867 cnfldbas 14869 mpocnfldadd 14870 mpocnfldmul 14872 cnfldcj 14874 expghmap 14914 lmfval 15217 lmbrf 15239 lmfss 15268 lmres 15272 lmtopcnp 15274 cnmet 15554 cncfval 15596 elcncf 15597 limcrcl 15682 limccl 15683 ellimc3apf 15684 limccnp2lem 15700 limccnp2cntop 15701 reldvg 15703 dvfvalap 15705 dvbss 15709 dvidlemap 15715 dvidrelem 15716 dvidsslem 15717 dvcnp2cntop 15723 dvaddxxbr 15725 dvmulxxbr 15726 dvaddxx 15727 dvmulxx 15728 dviaddf 15729 dvimulf 15730 dvcoapbr 15731 dvcjbr 15732 dvcj 15733 dvfre 15734 dvexp 15735 dvrecap 15737 dvmptclx 15742 dvef 15751 plyval 15756 elply 15758 elply2 15759 plyf 15761 plyss 15762 elplyr 15764 plyaddlem1 15771 plymullem1 15772 plyaddlem 15773 plymullem 15774 plysub 15777 plycolemc 15782 plyco 15783 plycj 15785 |
| Copyright terms: Public domain | W3C validator |