Theorem eqfnovd

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

	Ref	Expression
Hypotheses	eqfnovd.1	⊢ ( 𝜑 → 𝐹 Fn ( 𝐴 × 𝐵 ) )
	eqfnovd.2	⊢ ( 𝜑 → 𝐺 Fn ( 𝐴 × 𝐵 ) )
	eqfnovd.3	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 𝐹 𝑦 ) = ( 𝑥 𝐺 𝑦 ) )
Assertion	eqfnovd	⊢ ( 𝜑 → 𝐹 = 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		eqfnovd.1	⊢ ( 𝜑 → 𝐹 Fn ( 𝐴 × 𝐵 ) )
2		eqfnovd.2	⊢ ( 𝜑 → 𝐺 Fn ( 𝐴 × 𝐵 ) )
3		eqfnovd.3	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 𝐹 𝑦 ) = ( 𝑥 𝐺 𝑦 ) )
4	3	ralrimivva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐹 𝑦 ) = ( 𝑥 𝐺 𝑦 ) )
5		eqfnov2	⊢ ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐺 Fn ( 𝐴 × 𝐵 ) ) → ( 𝐹 = 𝐺 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐹 𝑦 ) = ( 𝑥 𝐺 𝑦 ) ) )
6	1 2 5	syl2anc	⊢ ( 𝜑 → ( 𝐹 = 𝐺 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐹 𝑦 ) = ( 𝑥 𝐺 𝑦 ) ) )
7	4 6	mpbird	⊢ ( 𝜑 → 𝐹 = 𝐺 )