Metamath Proof Explorer

Theorem sspwi

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

Ref Expression
Hypothesis sspwi.1 
|- A C_ B
Assertion sspwi 
|- ~P A C_ ~P B

Proof

Step Hyp Ref Expression
1 sspwi.1 
 |-  A C_ B
2 sspw 
 |-  ( A C_ B -> ~P A C_ ~P B )
3 1 2 ax-mp 
 |-  ~P A C_ ~P B