This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 (A \subseteq B \to x \subseteq B)$
2	1	com12	$⊢ A \subseteq B \to (x \subseteq A \to x \subseteq B)$
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 (x \in 𝒫 A \to x \in 𝒫 B)$
6	5	ssrdv	$⊢ A \subseteq B \to 𝒫 A \subseteq 𝒫 B$