eqfnov

Description: Equality of two operations is determined by their values. (Contributed by NM, 1-Sep-2005)

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

Step	Hyp	Ref	Expression
1		eqfnfv2	$⊢ (F Fn (A \times B) \land G Fn (C \times D)) \to (F = G \leftrightarrow (A \times B = C \times D \land \forall z \in (A \times B) F (z) = G (z)))$
2		fveq2	$⊢ z = ⟨x, y⟩ \to F (z) = F (⟨x, y⟩)$
3		fveq2	$⊢ z = ⟨x, y⟩ \to G (z) = G (⟨x, y⟩)$
4	2 3	eqeq12d	$⊢ z = ⟨x, y⟩ \to (F (z) = G (z) \leftrightarrow F (⟨x, y⟩) = G (⟨x, y⟩))$
5		df-ov	$⊢ x F y = F (⟨x, y⟩)$
6		df-ov	$⊢ x G y = G (⟨x, y⟩)$
7	5 6	eqeq12i	$⊢ x F y = x G y \leftrightarrow F (⟨x, y⟩) = G (⟨x, y⟩)$
8	4 7	bitr4di	$⊢ z = ⟨x, y⟩ \to (F (z) = G (z) \leftrightarrow x F y = x G y)$
9	8	ralxp	$⊢ \forall z \in (A \times B) F (z) = G (z) \leftrightarrow \forall x \in A \forall y \in B x F y = x G y$
10	9	anbi2i	$⊢ (A \times B = C \times D \land \forall z \in (A \times B) F (z) = G (z)) \leftrightarrow (A \times B = C \times D \land \forall x \in A \forall y \in B x F y = x G y)$
11	1 10	bitrdi	$⊢ (F Fn (A \times B) \land G Fn (C \times D)) \to (F = G \leftrightarrow (A \times B = C \times D \land \forall x \in A \forall y \in B x F y = x G y))$

Metamath Proof Explorer