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	$$⊢\left(A\in C\wedge B\in D\right)\to A\left(x\in C,y\in D⟼xFy\right)B=AFB$$

Proof

Step	Hyp	Ref	Expression
1		oveq12	$$⊢\left(x=A\wedge y=B\right)\to xFy=AFB$$
2		eqid	$$⊢\left(x\in C,y\in D⟼xFy\right)=\left(x\in C,y\in D⟼xFy\right)$$
3		ovex	$$⊢AFB\in \mathrm{V}$$
4	1 2 3	ovmpoa	$$⊢\left(A\in C\wedge B\in D\right)\to A\left(x\in C,y\in D⟼xFy\right)B=AFB$$