eqfnovd

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

	Ref	Expression
Hypotheses	eqfnovd.1	$⊢ φ \to F Fn (A \times B)$
	eqfnovd.2	$⊢ φ \to G Fn (A \times B)$
	eqfnovd.3	$⊢ (φ \land (x \in A \land y \in B)) \to x F y = x G y$
Assertion	eqfnovd	$⊢ φ \to F = G$

Step	Hyp	Ref	Expression
1		eqfnovd.1	$⊢ φ \to F Fn (A \times B)$
2		eqfnovd.2	$⊢ φ \to G Fn (A \times B)$
3		eqfnovd.3	$⊢ (φ \land (x \in A \land y \in B)) \to x F y = x G y$
4	3	ralrimivva	$⊢ φ \to \forall x \in A \forall y \in B x F y = x G y$
5		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)$
6	1 2 5	syl2anc	$⊢ φ \to (F = G \leftrightarrow \forall x \in A \forall y \in B x F y = x G y)$
7	4 6	mpbird	$⊢ φ \to F = G$

Metamath Proof Explorer