Step |
Hyp |
Ref |
Expression |
1 |
|
f1ocpbl.f |
|- ( ph -> F : V -1-1-onto-> X ) |
2 |
|
f1of1 |
|- ( F : V -1-1-onto-> X -> F : V -1-1-> X ) |
3 |
1 2
|
syl |
|- ( ph -> F : V -1-1-> X ) |
4 |
3
|
3ad2ant1 |
|- ( ( ph /\ ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> F : V -1-1-> X ) |
5 |
|
simp2l |
|- ( ( ph /\ ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> A e. V ) |
6 |
|
simp3l |
|- ( ( ph /\ ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> C e. V ) |
7 |
|
f1fveq |
|- ( ( F : V -1-1-> X /\ ( A e. V /\ C e. V ) ) -> ( ( F ` A ) = ( F ` C ) <-> A = C ) ) |
8 |
4 5 6 7
|
syl12anc |
|- ( ( ph /\ ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( ( F ` A ) = ( F ` C ) <-> A = C ) ) |
9 |
|
simp2r |
|- ( ( ph /\ ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> B e. V ) |
10 |
|
simp3r |
|- ( ( ph /\ ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> D e. V ) |
11 |
|
f1fveq |
|- ( ( F : V -1-1-> X /\ ( B e. V /\ D e. V ) ) -> ( ( F ` B ) = ( F ` D ) <-> B = D ) ) |
12 |
4 9 10 11
|
syl12anc |
|- ( ( ph /\ ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( ( F ` B ) = ( F ` D ) <-> B = D ) ) |
13 |
8 12
|
anbi12d |
|- ( ( ph /\ ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( ( ( F ` A ) = ( F ` C ) /\ ( F ` B ) = ( F ` D ) ) <-> ( A = C /\ B = D ) ) ) |