Metamath Proof Explorer

Theorem pweqi

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

Ref Expression
Hypothesis pweqi.1 
|- A = B
Assertion pweqi 
|- ~P A = ~P B

Proof

Step Hyp Ref Expression
1 pweqi.1 
 |-  A = B
2 pweq 
 |-  ( A = B -> ~P A = ~P B )
3 1 2 ax-mp 
 |-  ~P A = ~P B