Theorem eqfnovd

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

	Ref	Expression
Hypotheses	eqfnovd.1	|- ( ph -> F Fn ( A X. B ) )
	eqfnovd.2	|- ( ph -> G Fn ( A X. B ) )
	eqfnovd.3	|- ( ( ph /\ ( x e. A /\ y e. B ) ) -> ( x F y ) = ( x G y ) )
Assertion	eqfnovd	|- ( ph -> F = G )

Proof

Step	Hyp	Ref	Expression
1		eqfnovd.1	|- ( ph -> F Fn ( A X. B ) )
2		eqfnovd.2	|- ( ph -> G Fn ( A X. B ) )
3		eqfnovd.3	|- ( ( ph /\ ( x e. A /\ y e. B ) ) -> ( x F y ) = ( x G y ) )
4	3	ralrimivva	|- ( ph -> A. x e. A A. y e. B ( x F y ) = ( x G y ) )
5		eqfnov2	|- ( ( F Fn ( A X. B ) /\ G Fn ( A X. B ) ) -> ( F = G <-> A. x e. A A. y e. B ( x F y ) = ( x G y ) ) )
6	1 2 5	syl2anc	|- ( ph -> ( F = G <-> A. x e. A A. y e. B ( x F y ) = ( x G y ) ) )
7	4 6	mpbird	|- ( ph -> F = G )