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

Metamath Proof Explorer

Theorem eqfnov

Description: Equality of two operations is determined by their values. (Contributed by NM, 1-Sep-2005)

Ref Expression
Assertion eqfnov ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐺 Fn ( 𝐶 × 𝐷 ) ) → ( 𝐹 = 𝐺 ↔ ( ( 𝐴 × 𝐵 ) = ( 𝐶 × 𝐷 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐹 𝑦 ) = ( 𝑥 𝐺 𝑦 ) ) ) )

Proof

Step Hyp Ref Expression
1 eqfnfv2 ⊢ ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐺 Fn ( 𝐶 × 𝐷 ) ) → ( 𝐹 = 𝐺 ↔ ( ( 𝐴 × 𝐵 ) = ( 𝐶 × 𝐷 ) ∧ ∀ 𝑧 ∈ ( 𝐴 × 𝐵 ) ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) ) )
2 fveq2 ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
3 fveq2 ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
4 2 3 eqeq12d ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ↔ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = ( 𝐺 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) )
5 df-ov ⊢ ( 𝑥 𝐹 𝑦 ) = ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ )
6 df-ov ⊢ ( 𝑥 𝐺 𝑦 ) = ( 𝐺 ‘ ⟨ 𝑥 , 𝑦 ⟩ )
7 5 6 eqeq12i ⊢ ( ( 𝑥 𝐹 𝑦 ) = ( 𝑥 𝐺 𝑦 ) ↔ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = ( 𝐺 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
8 4 7 bitr4di ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ↔ ( 𝑥 𝐹 𝑦 ) = ( 𝑥 𝐺 𝑦 ) ) )
9 8 ralxp ⊢ ( ∀ 𝑧 ∈ ( 𝐴 × 𝐵 ) ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐹 𝑦 ) = ( 𝑥 𝐺 𝑦 ) )
10 9 anbi2i ⊢ ( ( ( 𝐴 × 𝐵 ) = ( 𝐶 × 𝐷 ) ∧ ∀ 𝑧 ∈ ( 𝐴 × 𝐵 ) ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) ↔ ( ( 𝐴 × 𝐵 ) = ( 𝐶 × 𝐷 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐹 𝑦 ) = ( 𝑥 𝐺 𝑦 ) ) )
11 1 10 bitrdi ⊢ ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐺 Fn ( 𝐶 × 𝐷 ) ) → ( 𝐹 = 𝐺 ↔ ( ( 𝐴 × 𝐵 ) = ( 𝐶 × 𝐷 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐹 𝑦 ) = ( 𝑥 𝐺 𝑦 ) ) ) )