Metamath Proof Explorer

Theorem pweqd

Description: Equality deduction for power class. (Contributed by NM, 27-Nov-2013)

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

Proof

Step Hyp Ref Expression
1 pweqd.1 
 |-  ( ph -> A = B )
2 pweq 
 |-  ( A = B -> ~P A = ~P B )
3 1 2 syl 
 |-  ( ph -> ~P A = ~P B )