Theorem elpwd

Description: Membership in a power class. (Contributed by Glauco Siliprandi, 11-Oct-2020)

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

Proof

Step	Hyp	Ref	Expression
1		elpwd.1	$$⊢\phi \to A\in V$$
2		elpwd.2	$$⊢\phi \to A\subseteq B$$
3		elpwg	$$⊢A\in V\to \left(A\in 𝒫B\leftrightarrow A\subseteq B\right)$$
4	1 3	syl	$$⊢\phi \to \left(A\in 𝒫B\leftrightarrow A\subseteq B\right)$$
5	2 4	mpbird	$$⊢\phi \to A\in 𝒫B$$