Theorem sselpwd

Description: Membership in a power set. (Contributed by Thierry Arnoux, 18-May-2020)

	Ref	Expression
Hypotheses	sselpwd.1	$$⊢\phi \to B\in V$$
	sselpwd.2	$$⊢\phi \to A\subseteq B$$
Assertion	sselpwd	$$⊢\phi \to A\in 𝒫B$$

Proof

Step	Hyp	Ref	Expression
1		sselpwd.1	$$⊢\phi \to B\in V$$
2		sselpwd.2	$$⊢\phi \to A\subseteq B$$
3	1 2	ssexd	$$⊢\phi \to A\in \mathrm{V}$$
4	3 2	elpwd	$$⊢\phi \to A\in 𝒫B$$