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	⊢ ( 𝜑 → 𝑅 ∈ 𝐴 )
	mpofvopd.2	⊢ ( 𝜑 → 𝑆 ∈ 𝐵 )
	mpofvopd.3	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
	mpofvopd.4	⊢ ( ( 𝜑 ∧ ⟨ 𝑅 , 𝑆 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) → 𝑌 = 𝐶 )
	mpofvopd.5	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
Assertion	mpofvopd	⊢ ( 𝜑 → ( 𝐹 ‘ ⟨ 𝑅 , 𝑆 ⟩ ) = 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		mpofvopd.1	⊢ ( 𝜑 → 𝑅 ∈ 𝐴 )
2		mpofvopd.2	⊢ ( 𝜑 → 𝑆 ∈ 𝐵 )
3		mpofvopd.3	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
4		mpofvopd.4	⊢ ( ( 𝜑 ∧ ⟨ 𝑅 , 𝑆 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) → 𝑌 = 𝐶 )
5		mpofvopd.5	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
6	1 2	opelxpd	⊢ ( 𝜑 → ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝐴 × 𝐵 ) )
7	6 3 4 5	mpofvd	⊢ ( 𝜑 → ( 𝐹 ‘ ⟨ 𝑅 , 𝑆 ⟩ ) = 𝑌 )