Theorem f1resveqaeq

Description: If a function restricted to a class is one-to-one, then for any two elements of the class, the values of the function at those elements are equal only if the two elements are the same element. (Contributed by BTernaryTau, 27-Sep-2023)

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

Proof

Step	Hyp	Ref	Expression
1		fvres	⊢ ( 𝐶 ∈ 𝐴 → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝐶 ) = ( 𝐹 ‘ 𝐶 ) )
2	1	ad2antrl	⊢ ( ( ( 𝐹 ↾ 𝐴 ) : 𝐴 –1-1→ 𝐵 ∧ ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝐶 ) = ( 𝐹 ‘ 𝐶 ) )
3		fvres	⊢ ( 𝐷 ∈ 𝐴 → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝐷 ) = ( 𝐹 ‘ 𝐷 ) )
4	3	ad2antll	⊢ ( ( ( 𝐹 ↾ 𝐴 ) : 𝐴 –1-1→ 𝐵 ∧ ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝐷 ) = ( 𝐹 ‘ 𝐷 ) )
5	2 4	eqeq12d	⊢ ( ( ( 𝐹 ↾ 𝐴 ) : 𝐴 –1-1→ 𝐵 ∧ ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝐶 ) = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝐷 ) ↔ ( 𝐹 ‘ 𝐶 ) = ( 𝐹 ‘ 𝐷 ) ) )
6		f1veqaeq	⊢ ( ( ( 𝐹 ↾ 𝐴 ) : 𝐴 –1-1→ 𝐵 ∧ ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝐶 ) = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝐷 ) → 𝐶 = 𝐷 ) )
7	5 6	sylbird	⊢ ( ( ( 𝐹 ↾ 𝐴 ) : 𝐴 –1-1→ 𝐵 ∧ ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝐶 ) = ( 𝐹 ‘ 𝐷 ) → 𝐶 = 𝐷 ) )