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 syl5ib
 |-  ( ( 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 ) )