Metamath Proof Explorer


Theorem sspwd

Description: The powerclass preserves inclusion (deduction form). (Contributed by BJ, 13-Apr-2024)

Ref Expression
Hypothesis sspwd.1 ( 𝜑𝐴𝐵 )
Assertion sspwd ( 𝜑 → 𝒫 𝐴 ⊆ 𝒫 𝐵 )

Proof

Step Hyp Ref Expression
1 sspwd.1 ( 𝜑𝐴𝐵 )
2 sspw ( 𝐴𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵 )
3 1 2 syl ( 𝜑 → 𝒫 𝐴 ⊆ 𝒫 𝐵 )