eqfnfv

Description: Equality of functions is determined by their values. Special case of Exercise 4 of TakeutiZaring p. 28 (with domain equality omitted). (Contributed by NM, 3-Aug-1994) (Proof shortened by Andrew Salmon, 22-Oct-2011) (Proof shortened by Mario Carneiro, 31-Aug-2015)

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

Proof

Step	Hyp	Ref	Expression
1		dffn5	$⊢ F Fn A \leftrightarrow F = (x \in A ⟼ F (x))$
2		dffn5	$⊢ G Fn A \leftrightarrow G = (x \in A ⟼ G (x))$
3		eqeq12	$⊢ (F = (x \in A ⟼ F (x)) \land G = (x \in A ⟼ G (x))) \to (F = G \leftrightarrow (x \in A ⟼ F (x)) = (x \in A ⟼ G (x)))$
4	1 2 3	syl2anb	$⊢ (F Fn A \land G Fn A) \to (F = G \leftrightarrow (x \in A ⟼ F (x)) = (x \in A ⟼ G (x)))$
5		fvex	$⊢ F (x) \in V$
6	5	rgenw	$⊢ \forall x \in A F (x) \in V$
7		mpteqb	$⊢ \forall x \in A F (x) \in V \to ((x \in A ⟼ F (x)) = (x \in A ⟼ G (x)) \leftrightarrow \forall x \in A F (x) = G (x))$
8	6 7	ax-mp	$⊢ (x \in A ⟼ F (x)) = (x \in A ⟼ G (x)) \leftrightarrow \forall x \in A F (x) = G (x)$
9	4 8	bitrdi	$⊢ (F Fn A \land G Fn A) \to (F = G \leftrightarrow \forall x \in A F (x) = G (x))$

Metamath Proof Explorer

Theorem eqfnfv

Proof