Step |
Hyp |
Ref |
Expression |
1 |
|
dff13 |
|- ( F : A -1-1-> B <-> ( F : A --> B /\ A. c e. A A. d e. A ( ( F ` c ) = ( F ` d ) -> c = d ) ) ) |
2 |
|
fveqeq2 |
|- ( c = C -> ( ( F ` c ) = ( F ` d ) <-> ( F ` C ) = ( F ` d ) ) ) |
3 |
|
eqeq1 |
|- ( c = C -> ( c = d <-> C = d ) ) |
4 |
2 3
|
imbi12d |
|- ( c = C -> ( ( ( F ` c ) = ( F ` d ) -> c = d ) <-> ( ( F ` C ) = ( F ` d ) -> C = d ) ) ) |
5 |
|
fveq2 |
|- ( d = D -> ( F ` d ) = ( F ` D ) ) |
6 |
5
|
eqeq2d |
|- ( d = D -> ( ( F ` C ) = ( F ` d ) <-> ( F ` C ) = ( F ` D ) ) ) |
7 |
|
eqeq2 |
|- ( d = D -> ( C = d <-> C = D ) ) |
8 |
6 7
|
imbi12d |
|- ( d = D -> ( ( ( F ` C ) = ( F ` d ) -> C = d ) <-> ( ( F ` C ) = ( F ` D ) -> C = D ) ) ) |
9 |
4 8
|
rspc2v |
|- ( ( C e. A /\ D e. A ) -> ( A. c e. A A. d e. A ( ( F ` c ) = ( F ` d ) -> c = d ) -> ( ( F ` C ) = ( F ` D ) -> C = D ) ) ) |
10 |
9
|
com12 |
|- ( A. c e. A A. d e. A ( ( F ` c ) = ( F ` d ) -> c = d ) -> ( ( C e. A /\ D e. A ) -> ( ( F ` C ) = ( F ` D ) -> C = D ) ) ) |
11 |
1 10
|
simplbiim |
|- ( F : A -1-1-> B -> ( ( C e. A /\ D e. A ) -> ( ( F ` C ) = ( F ` D ) -> C = D ) ) ) |
12 |
11
|
imp |
|- ( ( F : A -1-1-> B /\ ( C e. A /\ D e. A ) ) -> ( ( F ` C ) = ( F ` D ) -> C = D ) ) |