Theorem sspw

Description: The powerclass preserves inclusion. See sspwb for the biconditional version. (Contributed by NM, 13-Oct-1996) Extract forward implication of sspwb since it requires fewer axioms. (Revised by BJ, 13-Apr-2024)

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

Proof

Step	Hyp	Ref	Expression
1		sstr2	$$⊢x\subseteq A\to \left(A\subseteq B\to x\subseteq B\right)$$
2	1	com12	$$⊢A\subseteq B\to \left(x\subseteq A\to x\subseteq B\right)$$
3		velpw	$$⊢x\in 𝒫A\leftrightarrow x\subseteq A$$
4		velpw	$$⊢x\in 𝒫B\leftrightarrow x\subseteq B$$
5	2 3 4	3imtr4g	$$⊢A\subseteq B\to \left(x\in 𝒫A\to x\in 𝒫B\right)$$
6	5	ssrdv	$$⊢A\subseteq B\to 𝒫A\subseteq 𝒫B$$