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

Proof

Step	Hyp	Ref	Expression
1		mpt3fvotd.1	$$⊢\phi \to R\in A$$
2		mpt3fvotd.2	$$⊢\phi \to S\in B$$
3		mpt3fvotd.3	$$⊢\phi \to T\in C$$
4		mpt3fvotd.4	$$⊢\phi \to Y\in V$$
5		mpt3fvotd.5	$$⊢\left(\phi \wedge ⟨R,S,T⟩=⟨x,y,z⟩\right)\to Y=D$$
6		mpt3fvotd.6	$$⊢F=\left(x\in A,y\in B,z\in C⟼D\right)$$
7		otelxp	$$⊢⟨R,S,T⟩\in \left(\left(A\times B\right)\times C\right)\leftrightarrow \left(R\in A\wedge S\in B\wedge T\in C\right)$$
8	1 2 3 7	syl3anbrc	$$⊢\phi \to ⟨R,S,T⟩\in \left(\left(A\times B\right)\times C\right)$$
9	8 4 5 6	mpt3fvd	$$⊢\phi \to F\left(⟨R,S,T⟩\right)=Y$$