Metamath Proof Explorer

Theorem neg11

Description: Negative is one-to-one. (Contributed by NM, 8-Feb-2005) (Revised by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion neg11 
|- ( ( A e. CC /\ B e. CC ) -> ( -u A = -u B <-> A = B ) )

Proof

Step Hyp Ref Expression
1 negeq 
 |-  ( -u A = -u B -> -u -u A = -u -u B )
2 negneg 
 |-  ( A e. CC -> -u -u A = A )
3 negneg 
 |-  ( B e. CC -> -u -u B = B )
4 2 3 eqeqan12d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( -u -u A = -u -u B <-> A = B ) )
5 1 4 imbitrid 
 |-  ( ( A e. CC /\ B e. CC ) -> ( -u A = -u B -> A = B ) )
6 negeq 
 |-  ( A = B -> -u A = -u B )
7 5 6 impbid1 
 |-  ( ( A e. CC /\ B e. CC ) -> ( -u A = -u B <-> A = B ) )