Theorem f1fveq

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

	Ref	Expression
Assertion	f1fveq	$$⊢\left(F:A\underset{1-1}{⟶}B\wedge \left(C\in A\wedge D\in A\right)\right)\to \left(F\left(C\right)=F\left(D\right)\leftrightarrow C=D\right)$$

Proof

Step	Hyp	Ref	Expression
1		f1veqaeq	$$⊢\left(F:A\underset{1-1}{⟶}B\wedge \left(C\in A\wedge D\in A\right)\right)\to \left(F\left(C\right)=F\left(D\right)\to C=D\right)$$
2		fveq2	$$⊢C=D\to F\left(C\right)=F\left(D\right)$$
3	1 2	impbid1	$$⊢\left(F:A\underset{1-1}{⟶}B\wedge \left(C\in A\wedge D\in A\right)\right)\to \left(F\left(C\right)=F\left(D\right)\leftrightarrow C=D\right)$$