Theorem f1fveq

Description: Equality of function values for a one-to-one function. (Contributed by NM, 11-Feb-1997)

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

Proof

Step	Hyp	Ref	Expression
1		f1veqaeq	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝐶 ) = ( 𝐹 ‘ 𝐷 ) → 𝐶 = 𝐷 ) )
2		fveq2	⊢ ( 𝐶 = 𝐷 → ( 𝐹 ‘ 𝐶 ) = ( 𝐹 ‘ 𝐷 ) )
3	1 2	impbid1	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝐶 ) = ( 𝐹 ‘ 𝐷 ) ↔ 𝐶 = 𝐷 ) )