Metamath Proof Explorer


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 ( ( 𝐹 : 𝐴1-1-onto𝐵𝐶𝐴 ) → ( ( 𝐹𝐶 ) = 𝐷 → ( 𝐹𝐷 ) = 𝐶 ) )

Proof

Step Hyp Ref Expression
1 fveq2 ( 𝐷 = ( 𝐹𝐶 ) → ( 𝐹𝐷 ) = ( 𝐹 ‘ ( 𝐹𝐶 ) ) )
2 1 eqcoms ( ( 𝐹𝐶 ) = 𝐷 → ( 𝐹𝐷 ) = ( 𝐹 ‘ ( 𝐹𝐶 ) ) )
3 f1ocnvfv1 ( ( 𝐹 : 𝐴1-1-onto𝐵𝐶𝐴 ) → ( 𝐹 ‘ ( 𝐹𝐶 ) ) = 𝐶 )
4 3 eqeq2d ( ( 𝐹 : 𝐴1-1-onto𝐵𝐶𝐴 ) → ( ( 𝐹𝐷 ) = ( 𝐹 ‘ ( 𝐹𝐶 ) ) ↔ ( 𝐹𝐷 ) = 𝐶 ) )
5 2 4 syl5ib ( ( 𝐹 : 𝐴1-1-onto𝐵𝐶𝐴 ) → ( ( 𝐹𝐶 ) = 𝐷 → ( 𝐹𝐷 ) = 𝐶 ) )