This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem f1fveq

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

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

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