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

Metamath Proof Explorer

Theorem eqfnov2

Description: Two operators with the same domain are equal iff their values at each point in the domain are equal. (Contributed by Jeff Madsen, 7-Jun-2010)

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

Proof

Step	Hyp	Ref	Expression
1		eqfnov	$⊢ (F Fn (A \times B) \land G Fn (A \times B)) \to (F = G \leftrightarrow (A \times B = A \times B \land \forall x \in A \forall y \in B x F y = x G y))$
2		simpr	$⊢ (A \times B = A \times B \land \forall x \in A \forall y \in B x F y = x G y) \to \forall x \in A \forall y \in B x F y = x G y$
3		eqidd	$⊢ \forall x \in A \forall y \in B x F y = x G y \to A \times B = A \times B$
4	3	ancri	$⊢ \forall x \in A \forall y \in B x F y = x G y \to (A \times B = A \times B \land \forall x \in A \forall y \in B x F y = x G y)$
5	2 4	impbii	$⊢ (A \times B = A \times B \land \forall x \in A \forall y \in B x F y = x G y) \leftrightarrow \forall x \in A \forall y \in B x F y = x G y$
6	1 5	bitrdi	$⊢ (F Fn (A \times B) \land G Fn (A \times B)) \to (F = G \leftrightarrow \forall x \in A \forall y \in B x F y = x G y)$