This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

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