Theorem eqfnovd

Description: Deduction for equality of operations. (Contributed by Zhi Wang, 19-Nov-2025)

	Ref	Expression
Hypotheses	eqfnovd.1	$$⊢\phi \to FFn\left(A\times B\right)$$
	eqfnovd.2	$$⊢\phi \to GFn\left(A\times B\right)$$
	eqfnovd.3	$$⊢\left(\phi \wedge \left(x\in A\wedge y\in B\right)\right)\to xFy=xGy$$
Assertion	eqfnovd	$$⊢\phi \to F=G$$

Proof

Step	Hyp	Ref	Expression
1		eqfnovd.1	$$⊢\phi \to FFn\left(A\times B\right)$$
2		eqfnovd.2	$$⊢\phi \to GFn\left(A\times B\right)$$
3		eqfnovd.3	$$⊢\left(\phi \wedge \left(x\in A\wedge y\in B\right)\right)\to xFy=xGy$$
4	3	ralrimivva	$$⊢\phi \to \forall x\in A\forall y\in BxFy=xGy$$
5		eqfnov2	$$⊢\left(FFn\left(A\times B\right)\wedge GFn\left(A\times B\right)\right)\to \left(F=G\leftrightarrow \forall x\in A\forall y\in BxFy=xGy\right)$$
6	1 2 5	syl2anc	$$⊢\phi \to \left(F=G\leftrightarrow \forall x\in A\forall y\in BxFy=xGy\right)$$
7	4 6	mpbird	$$⊢\phi \to F=G$$