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	imbitrid	⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐶 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝐶 ) = 𝐷 → ( ◡ 𝐹 ‘ 𝐷 ) = 𝐶 ) )