Metamath Proof Explorer

Theorem eqfnfv2

Description: Equality of functions is determined by their values. Exercise 4 of TakeutiZaring p. 28. (Contributed by NM, 3-Aug-1994) (Revised by Mario Carneiro, 31-Aug-2015)

		Ref	Expression
	Assertion	eqfnfv2	$⊢ (F Fn A \land G Fn B) \to (F = G \leftrightarrow (A = B \land \forall x \in A F (x) = G (x)))$

Proof

Step	Hyp	Ref	Expression
1		dmeq	$⊢ F = G \to dom F = dom G$
2		fndm	$⊢ F Fn A \to dom F = A$
3		fndm	$⊢ G Fn B \to dom G = B$
4	2 3	eqeqan12d	$⊢ (F Fn A \land G Fn B) \to (dom F = dom G \leftrightarrow A = B)$
5	1 4	imbitrid	$⊢ (F Fn A \land G Fn B) \to (F = G \to A = B)$
6	5	pm4.71rd	$⊢ (F Fn A \land G Fn B) \to (F = G \leftrightarrow (A = B \land F = G))$
7		fneq2	$⊢ A = B \to (G Fn A \leftrightarrow G Fn B)$
8	7	biimparc	$⊢ (G Fn B \land A = B) \to G Fn A$
9		eqfnfv	$⊢ (F Fn A \land G Fn A) \to (F = G \leftrightarrow \forall x \in A F (x) = G (x))$
10	8 9	sylan2	$⊢ (F Fn A \land (G Fn B \land A = B)) \to (F = G \leftrightarrow \forall x \in A F (x) = G (x))$
11	10	anassrs	$⊢ ((F Fn A \land G Fn B) \land A = B) \to (F = G \leftrightarrow \forall x \in A F (x) = G (x))$
12	11	pm5.32da	$⊢ (F Fn A \land G Fn B) \to ((A = B \land F = G) \leftrightarrow (A = B \land \forall x \in A F (x) = G (x)))$
13	6 12	bitrd	$⊢ (F Fn A \land G Fn B) \to (F = G \leftrightarrow (A = B \land \forall x \in A F (x) = G (x)))$