Theorem f1ocnvfvrneq

Description: If the values of a one-to-one function for two arguments from the range of the function are equal, the arguments themselves must be equal. (Contributed by Alexander van der Vekens, 12-Nov-2017)

	Ref	Expression
Assertion	f1ocnvfvrneq	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ( 𝐶 ∈ ran 𝐹 ∧ 𝐷 ∈ ran 𝐹 ) ) → ( ( ◡ 𝐹 ‘ 𝐶 ) = ( ◡ 𝐹 ‘ 𝐷 ) → 𝐶 = 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		f1f1orn	⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → 𝐹 : 𝐴 –1-1-onto→ ran 𝐹 )
2		f1ocnv	⊢ ( 𝐹 : 𝐴 –1-1-onto→ ran 𝐹 → ◡ 𝐹 : ran 𝐹 –1-1-onto→ 𝐴 )
3		f1of1	⊢ ( ◡ 𝐹 : ran 𝐹 –1-1-onto→ 𝐴 → ◡ 𝐹 : ran 𝐹 –1-1→ 𝐴 )
4		f1veqaeq	⊢ ( ( ◡ 𝐹 : ran 𝐹 –1-1→ 𝐴 ∧ ( 𝐶 ∈ ran 𝐹 ∧ 𝐷 ∈ ran 𝐹 ) ) → ( ( ◡ 𝐹 ‘ 𝐶 ) = ( ◡ 𝐹 ‘ 𝐷 ) → 𝐶 = 𝐷 ) )
5	4	ex	⊢ ( ◡ 𝐹 : ran 𝐹 –1-1→ 𝐴 → ( ( 𝐶 ∈ ran 𝐹 ∧ 𝐷 ∈ ran 𝐹 ) → ( ( ◡ 𝐹 ‘ 𝐶 ) = ( ◡ 𝐹 ‘ 𝐷 ) → 𝐶 = 𝐷 ) ) )
6	1 2 3 5	4syl	⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → ( ( 𝐶 ∈ ran 𝐹 ∧ 𝐷 ∈ ran 𝐹 ) → ( ( ◡ 𝐹 ‘ 𝐶 ) = ( ◡ 𝐹 ‘ 𝐷 ) → 𝐶 = 𝐷 ) ) )
7	6	imp	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ( 𝐶 ∈ ran 𝐹 ∧ 𝐷 ∈ ran 𝐹 ) ) → ( ( ◡ 𝐹 ‘ 𝐶 ) = ( ◡ 𝐹 ‘ 𝐷 ) → 𝐶 = 𝐷 ) )