Theorem mpofvopd

Description: Value of a two-argument function (usually an operation) in maps-to notation at an ordered pair. (Contributed by BTernaryTau, 18-Oct-2026)

	Ref	Expression
Hypotheses	mpofvopd.1	|- ( ph -> R e. A )
	mpofvopd.2	|- ( ph -> S e. B )
	mpofvopd.3	|- ( ph -> Y e. V )
	mpofvopd.4	|- ( ( ph /\ <. R , S >. = <. x , y >. ) -> Y = C )
	mpofvopd.5	|- F = ( x e. A , y e. B |-> C )
Assertion	mpofvopd	|- ( ph -> ( F ` <. R , S >. ) = Y )

Proof

Step	Hyp	Ref	Expression
1		mpofvopd.1	|- ( ph -> R e. A )
2		mpofvopd.2	|- ( ph -> S e. B )
3		mpofvopd.3	|- ( ph -> Y e. V )
4		mpofvopd.4	|- ( ( ph /\ <. R , S >. = <. x , y >. ) -> Y = C )
5		mpofvopd.5	|- F = ( x e. A , y e. B |-> C )
6	1 2	opelxpd	|- ( ph -> <. R , S >. e. ( A X. B ) )
7	6 3 4 5	mpofvd	|- ( ph -> ( F ` <. R , S >. ) = Y )