Theorem ovmpot

Description: The value of an operation is equal to the value of the same operation expressed in maps-to notation. (Contributed by GG, 16-Mar-2025) (Revised by GG, 13-Apr-2025)

	Ref	Expression
Assertion	ovmpot	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( 𝐴 ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ ( 𝑥 𝐹 𝑦 ) ) 𝐵 ) = ( 𝐴 𝐹 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		oveq12	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑥 𝐹 𝑦 ) = ( 𝐴 𝐹 𝐵 ) )
2		eqid	⊢ ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ ( 𝑥 𝐹 𝑦 ) ) = ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ ( 𝑥 𝐹 𝑦 ) )
3		ovex	⊢ ( 𝐴 𝐹 𝐵 ) ∈ V
4	1 2 3	ovmpoa	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( 𝐴 ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ ( 𝑥 𝐹 𝑦 ) ) 𝐵 ) = ( 𝐴 𝐹 𝐵 ) )