![]() |
Mathbox for Glauco Siliprandi |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > elpwinss | Structured version Visualization version GIF version |
Description: An element of the powerset of 𝐵 intersected with anything, is a subset of 𝐵. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Ref | Expression |
---|---|
elpwinss | ⊢ (𝐴 ∈ (𝒫 𝐵 ∩ 𝐶) → 𝐴 ⊆ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elinel1 4154 | . 2 ⊢ (𝐴 ∈ (𝒫 𝐵 ∩ 𝐶) → 𝐴 ∈ 𝒫 𝐵) | |
2 | 1 | elpwid 4568 | 1 ⊢ (𝐴 ∈ (𝒫 𝐵 ∩ 𝐶) → 𝐴 ⊆ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2106 ∩ cin 3908 ⊆ wss 3909 𝒫 cpw 4559 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2707 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2714 df-cleq 2728 df-clel 2814 df-v 3446 df-in 3916 df-ss 3926 df-pw 4561 |
This theorem is referenced by: sge0z 44586 sge0revalmpt 44589 sge0f1o 44593 sge0rnbnd 44604 sge0pnffigt 44607 sge0lefi 44609 sge0ltfirp 44611 sge0gerpmpt 44613 sge0le 44618 sge0ltfirpmpt 44619 sge0iunmptlemre 44626 sge0rpcpnf 44632 sge0lefimpt 44634 sge0ltfirpmpt2 44637 sge0isum 44638 sge0xaddlem1 44644 sge0xaddlem2 44645 sge0pnffigtmpt 44651 sge0pnffsumgt 44653 sge0gtfsumgt 44654 sge0uzfsumgt 44655 sge0seq 44657 sge0reuz 44658 omeiunltfirp 44730 carageniuncllem2 44733 caratheodorylem2 44738 |
Copyright terms: Public domain | W3C validator |