Theorem mpt3fvotd

Description: Value of a three-argument function in maps-to notation at an ordered triple. (Contributed by BTernaryTau, 28-Sep-2026)

	Ref	Expression
Hypotheses	mpt3fvotd.1	⊢ ( 𝜑 → 𝑅 ∈ 𝐴 )
	mpt3fvotd.2	⊢ ( 𝜑 → 𝑆 ∈ 𝐵 )
	mpt3fvotd.3	⊢ ( 𝜑 → 𝑇 ∈ 𝐶 )
	mpt3fvotd.4	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
	mpt3fvotd.5	⊢ ( ( 𝜑 ∧ ⟨ 𝑅 , 𝑆 , 𝑇 ⟩ = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) → 𝑌 = 𝐷 )
	mpt3fvotd.6	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐶 ↦ 𝐷 )
Assertion	mpt3fvotd	⊢ ( 𝜑 → ( 𝐹 ‘ ⟨ 𝑅 , 𝑆 , 𝑇 ⟩ ) = 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		mpt3fvotd.1	⊢ ( 𝜑 → 𝑅 ∈ 𝐴 )
2		mpt3fvotd.2	⊢ ( 𝜑 → 𝑆 ∈ 𝐵 )
3		mpt3fvotd.3	⊢ ( 𝜑 → 𝑇 ∈ 𝐶 )
4		mpt3fvotd.4	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
5		mpt3fvotd.5	⊢ ( ( 𝜑 ∧ ⟨ 𝑅 , 𝑆 , 𝑇 ⟩ = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) → 𝑌 = 𝐷 )
6		mpt3fvotd.6	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐶 ↦ 𝐷 )
7		otelxp	⊢ ( ⟨ 𝑅 , 𝑆 , 𝑇 ⟩ ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ↔ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐶 ) )
8	1 2 3 7	syl3anbrc	⊢ ( 𝜑 → ⟨ 𝑅 , 𝑆 , 𝑇 ⟩ ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) )
9	8 4 5 6	mpt3fvd	⊢ ( 𝜑 → ( 𝐹 ‘ ⟨ 𝑅 , 𝑆 , 𝑇 ⟩ ) = 𝑌 )