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 )