Metamath Proof Explorer

Theorem cj11

Description: Complex conjugate is a one-to-one function. (Contributed by NM, 29-Apr-2005) (Proof shortened by Eric Schmidt, 2-Jul-2009)

Ref Expression
Assertion cj11 
|- ( ( A e. CC /\ B e. CC ) -> ( ( * ` A ) = ( * ` B ) <-> A = B ) )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( ( * ` A ) = ( * ` B ) -> ( * ` ( * ` A ) ) = ( * ` ( * ` B ) ) )
2 cjcj 
 |-  ( A e. CC -> ( * ` ( * ` A ) ) = A )
3 cjcj 
 |-  ( B e. CC -> ( * ` ( * ` B ) ) = B )
4 2 3 eqeqan12d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( * ` ( * ` A ) ) = ( * ` ( * ` B ) ) <-> A = B ) )
5 1 4 syl5ib 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( * ` A ) = ( * ` B ) -> A = B ) )
6 fveq2 
 |-  ( A = B -> ( * ` A ) = ( * ` B ) )
7 5 6 impbid1 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( * ` A ) = ( * ` B ) <-> A = B ) )