Metamath Proof Explorer


Theorem elpwinss

Description: An element of the powerset of B intersected with anything, is a subset of B . (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Assertion elpwinss A𝒫BCAB

Proof

Step Hyp Ref Expression
1 elinel1 A𝒫BCA𝒫B
2 1 elpwid A𝒫BCAB