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	$$⊢\phi \to R\in A$$
	mpofvopd.2	$$⊢\phi \to S\in B$$
	mpofvopd.3	$$⊢\phi \to Y\in V$$
	mpofvopd.4	$$⊢\left(\phi \wedge ⟨R,S⟩=⟨x,y⟩\right)\to Y=C$$
	mpofvopd.5	$$⊢F=\left(x\in A,y\in B⟼C\right)$$
Assertion	mpofvopd	$$⊢\phi \to F\left(⟨R,S⟩\right)=Y$$

Proof

Step	Hyp	Ref	Expression
1		mpofvopd.1	$$⊢\phi \to R\in A$$
2		mpofvopd.2	$$⊢\phi \to S\in B$$
3		mpofvopd.3	$$⊢\phi \to Y\in V$$
4		mpofvopd.4	$$⊢\left(\phi \wedge ⟨R,S⟩=⟨x,y⟩\right)\to Y=C$$
5		mpofvopd.5	$$⊢F=\left(x\in A,y\in B⟼C\right)$$
6	1 2	opelxpd	$$⊢\phi \to ⟨R,S⟩\in \left(A\times B\right)$$
7	6 3 4 5	mpofvd	$$⊢\phi \to F\left(⟨R,S⟩\right)=Y$$