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 ( 𝐴𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵 )

Proof

Step Hyp Ref Expression
1 sstr2 ( 𝑥𝐴 → ( 𝐴𝐵𝑥𝐵 ) )
2 1 com12 ( 𝐴𝐵 → ( 𝑥𝐴𝑥𝐵 ) )
3 velpw ( 𝑥 ∈ 𝒫 𝐴𝑥𝐴 )
4 velpw ( 𝑥 ∈ 𝒫 𝐵𝑥𝐵 )
5 2 3 4 3imtr4g ( 𝐴𝐵 → ( 𝑥 ∈ 𝒫 𝐴𝑥 ∈ 𝒫 𝐵 ) )
6 5 ssrdv ( 𝐴𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵 )