This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ( 𝐴 × 𝐵 ) ) → ( 𝐹 = 𝐺 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐹 𝑦 ) = ( 𝑥 𝐺 𝑦 ) ) )