Metamath Proof Explorer


Theorem sspwd

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

Ref Expression
Hypothesis sspwd.1 φAB
Assertion sspwd φ𝒫A𝒫B

Proof

Step Hyp Ref Expression
1 sspwd.1 φAB
2 sspw AB𝒫A𝒫B
3 1 2 syl φ𝒫A𝒫B