Metamath Proof Explorer


Theorem sspwd

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

Ref Expression
Hypothesis sspwd.1
|- ( ph -> A C_ B )
Assertion sspwd
|- ( ph -> ~P A C_ ~P B )

Proof

Step Hyp Ref Expression
1 sspwd.1
 |-  ( ph -> A C_ B )
2 sspw
 |-  ( A C_ B -> ~P A C_ ~P B )
3 1 2 syl
 |-  ( ph -> ~P A C_ ~P B )