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