Theorem mpofvop2d

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

Proof

Step	Hyp	Ref	Expression
1		mpofvop2d.1	⊢ ( 𝜑 → 𝑅 ∈ 𝐴 )
2		mpofvop2d.2	⊢ ( 𝜑 → 𝑆 ∈ 𝐵 )
3		mpofvop2d.3	⊢ ( 𝜑 → 𝐿 ∈ 𝑉 )
4		mpofvop2d.4	⊢ ( ( 𝜑 ∧ 𝑅 = 𝑥 ) → 𝐾 = 𝐶 )
5		mpofvop2d.5	⊢ ( ( 𝜑 ∧ 𝑆 = 𝑦 ) → 𝐿 = 𝐾 )
6		mpofvop2d.6	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
7		opthg	⊢ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐵 ) → ( ⟨ 𝑅 , 𝑆 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ↔ ( 𝑅 = 𝑥 ∧ 𝑆 = 𝑦 ) ) )
8	1 2 7	syl2anc	⊢ ( 𝜑 → ( ⟨ 𝑅 , 𝑆 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ↔ ( 𝑅 = 𝑥 ∧ 𝑆 = 𝑦 ) ) )
9	4	ex	⊢ ( 𝜑 → ( 𝑅 = 𝑥 → 𝐾 = 𝐶 ) )
10	5	ex	⊢ ( 𝜑 → ( 𝑆 = 𝑦 → 𝐿 = 𝐾 ) )
11	9 10	anim12d	⊢ ( 𝜑 → ( ( 𝑅 = 𝑥 ∧ 𝑆 = 𝑦 ) → ( 𝐾 = 𝐶 ∧ 𝐿 = 𝐾 ) ) )
12	8 11	sylbid	⊢ ( 𝜑 → ( ⟨ 𝑅 , 𝑆 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐾 = 𝐶 ∧ 𝐿 = 𝐾 ) ) )
13		eqtr	⊢ ( ( 𝐿 = 𝐾 ∧ 𝐾 = 𝐶 ) → 𝐿 = 𝐶 )
14	13	ancoms	⊢ ( ( 𝐾 = 𝐶 ∧ 𝐿 = 𝐾 ) → 𝐿 = 𝐶 )
15	12 14	syl6	⊢ ( 𝜑 → ( ⟨ 𝑅 , 𝑆 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ → 𝐿 = 𝐶 ) )
16	15	imp	⊢ ( ( 𝜑 ∧ ⟨ 𝑅 , 𝑆 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) → 𝐿 = 𝐶 )
17	1 2 3 16 6	mpofvopd	⊢ ( 𝜑 → ( 𝐹 ‘ ⟨ 𝑅 , 𝑆 ⟩ ) = 𝐿 )