Theorem sspwimpALT2

Description: If a class is a subclass of another class, then its power class is a subclass of that other class's power class. Left-to-right implication of Exercise 18 of TakeutiZaring p. 18. Proof derived by completeusersproof.c from User's Proof in VirtualDeductionProofs.txt. The User's Proof in html format is displayed in https://us.metamath.org/other/completeusersproof/sspwimpaltvd.html . (Contributed by Alan Sare, 11-Sep-2016) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	sspwimpALT2	$$⊢A\subseteq B\to 𝒫A\subseteq 𝒫B$$

Proof

Step	Hyp	Ref	Expression
1		vex	$$⊢x\in \mathrm{V}$$
2		elpwi	$$⊢x\in 𝒫A\to x\subseteq A$$
3		id	$$⊢A\subseteq B\to A\subseteq B$$
4	2 3	sylan9ssr	$$⊢\left(A\subseteq B\wedge x\in 𝒫A\right)\to x\subseteq B$$
5		elpwg	$$⊢x\in \mathrm{V}\to \left(x\in 𝒫B\leftrightarrow x\subseteq B\right)$$
6	5	biimpar	$$⊢\left(x\in \mathrm{V}\wedge x\subseteq B\right)\to x\in 𝒫B$$
7	1 4 6	sylancr	$$⊢\left(A\subseteq B\wedge x\in 𝒫A\right)\to x\in 𝒫B$$
8	7	ex	$$⊢A\subseteq B\to \left(x\in 𝒫A\to x\in 𝒫B\right)$$
9	8	ssrdv	$$⊢A\subseteq B\to 𝒫A\subseteq 𝒫B$$