Metamath Proof Explorer

Theorem pweq

Description: Equality theorem for power class. (Contributed by NM, 21-Jun-1993) (Proof shortened by BJ, 13-Apr-2024)

Ref Expression
Assertion pweq 
|- ( A = B -> ~P A = ~P B )

Proof

Step Hyp Ref Expression
1 eqimss 
 |-  ( A = B -> A C_ B )
2 1 sspwd 
 |-  ( A = B -> ~P A C_ ~P B )
3 eqimss2 
 |-  ( A = B -> B C_ A )
4 3 sspwd 
 |-  ( A = B -> ~P B C_ ~P A )
5 2 4 eqssd 
 |-  ( A = B -> ~P A = ~P B )