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	|- ( ( A e. C /\ B e. D ) -> ( A ( x e. C , y e. D |-> ( x F y ) ) B ) = ( A F B ) )

Proof

Step	Hyp	Ref	Expression
1		oveq12	|- ( ( x = A /\ y = B ) -> ( x F y ) = ( A F B ) )
2		eqid	|- ( x e. C , y e. D |-> ( x F y ) ) = ( x e. C , y e. D |-> ( x F y ) )
3		ovex	|- ( A F B ) e. _V
4	1 2 3	ovmpoa	|- ( ( A e. C /\ B e. D ) -> ( A ( x e. C , y e. D |-> ( x F y ) ) B ) = ( A F B ) )