Theorem f1ocnvfv

Description: Relationship between the value of a one-to-one onto function and the value of its converse. (Contributed by Raph Levien, 10-Apr-2004)

	Ref	Expression
Assertion	f1ocnvfv	|- ( ( F : A -1-1-onto-> B /\ C e. A ) -> ( ( F ` C ) = D -> ( `' F ` D ) = C ) )

Proof

Step	Hyp	Ref	Expression
1		fveq2	|- ( D = ( F ` C ) -> ( `' F ` D ) = ( `' F ` ( F ` C ) ) )
2	1	eqcoms	|- ( ( F ` C ) = D -> ( `' F ` D ) = ( `' F ` ( F ` C ) ) )
3		f1ocnvfv1	|- ( ( F : A -1-1-onto-> B /\ C e. A ) -> ( `' F ` ( F ` C ) ) = C )
4	3	eqeq2d	|- ( ( F : A -1-1-onto-> B /\ C e. A ) -> ( ( `' F ` D ) = ( `' F ` ( F ` C ) ) <-> ( `' F ` D ) = C ) )
5	2 4	syl5ib	|- ( ( F : A -1-1-onto-> B /\ C e. A ) -> ( ( F ` C ) = D -> ( `' F ` D ) = C ) )