Theorem eqfnov2

Description: Two operators with the same domain are equal iff their values at each point in the domain are equal. (Contributed by Jeff Madsen, 7-Jun-2010)

	Ref	Expression
Assertion	eqfnov2	⊢ ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐺 Fn ( 𝐴 × 𝐵 ) ) → ( 𝐹 = 𝐺 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐹 𝑦 ) = ( 𝑥 𝐺 𝑦 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eqfnov	⊢ ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐺 Fn ( 𝐴 × 𝐵 ) ) → ( 𝐹 = 𝐺 ↔ ( ( 𝐴 × 𝐵 ) = ( 𝐴 × 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐹 𝑦 ) = ( 𝑥 𝐺 𝑦 ) ) ) )
2		simpr	⊢ ( ( ( 𝐴 × 𝐵 ) = ( 𝐴 × 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐹 𝑦 ) = ( 𝑥 𝐺 𝑦 ) ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐹 𝑦 ) = ( 𝑥 𝐺 𝑦 ) )
3		eqidd	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐹 𝑦 ) = ( 𝑥 𝐺 𝑦 ) → ( 𝐴 × 𝐵 ) = ( 𝐴 × 𝐵 ) )
4	3	ancri	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐹 𝑦 ) = ( 𝑥 𝐺 𝑦 ) → ( ( 𝐴 × 𝐵 ) = ( 𝐴 × 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐹 𝑦 ) = ( 𝑥 𝐺 𝑦 ) ) )
5	2 4	impbii	⊢ ( ( ( 𝐴 × 𝐵 ) = ( 𝐴 × 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐹 𝑦 ) = ( 𝑥 𝐺 𝑦 ) ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐹 𝑦 ) = ( 𝑥 𝐺 𝑦 ) )
6	1 5	bitrdi	⊢ ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐺 Fn ( 𝐴 × 𝐵 ) ) → ( 𝐹 = 𝐺 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐹 𝑦 ) = ( 𝑥 𝐺 𝑦 ) ) )