Theorem elpwi2OLD

Description: Obsolete version of elpwi2 as of 26-May-2024. (Contributed by Glauco Siliprandi, 3-Mar-2021) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	elpwi2.1	$$⊢B\in V$$
	elpwi2.2	$$⊢A\subseteq B$$
Assertion	elpwi2OLD	$$⊢A\in 𝒫B$$

Proof

Step	Hyp	Ref	Expression
1		elpwi2.1	$$⊢B\in V$$
2		elpwi2.2	$$⊢A\subseteq B$$
3		elpw2g	$$⊢B\in V\to \left(A\in 𝒫B\leftrightarrow A\subseteq B\right)$$
4	1 3	ax-mp	$$⊢A\in 𝒫B\leftrightarrow A\subseteq B$$
5	2 4	mpbir	$$⊢A\in 𝒫B$$