Theorem eqfnov

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

	Ref	Expression
Assertion	eqfnov	$$⊢\left(FFn\left(A\times B\right)\wedge GFn\left(C\times D\right)\right)\to \left(F=G\leftrightarrow \left(A\times B=C\times D\wedge \forall x\in A\forall y\in BxFy=xGy\right)\right)$$

Proof

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