Metamath Proof Explorer

Theorem xneg11

Description: Extended real version of neg11 . (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xneg11 
|- ( ( A e. RR* /\ B e. RR* ) -> ( -e A = -e B <-> A = B ) )

Proof

Step Hyp Ref Expression
1 xnegeq 
 |-  ( -e A = -e B -> -e -e A = -e -e B )
2 xnegneg 
 |-  ( A e. RR* -> -e -e A = A )
3 xnegneg 
 |-  ( B e. RR* -> -e -e B = B )
4 2 3 eqeqan12d 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( -e -e A = -e -e B <-> A = B ) )
5 1 4 imbitrid 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( -e A = -e B -> A = B ) )
6 xnegeq 
 |-  ( A = B -> -e A = -e B )
7 5 6 impbid1 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( -e A = -e B <-> A = B ) )