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