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