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\in \left(𝒫B\cap C\right)\to A\subseteq B$$

Proof

Step	Hyp	Ref	Expression
1		elinel1	$$⊢A\in \left(𝒫B\cap C\right)\to A\in 𝒫B$$
2	1	elpwid	$$⊢A\in \left(𝒫B\cap C\right)\to A\subseteq B$$