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	|- ( ph -> R e. A )
	mpt3fvotd.2	|- ( ph -> S e. B )
	mpt3fvotd.3	|- ( ph -> T e. C )
	mpt3fvotd.4	|- ( ph -> Y e. V )
	mpt3fvotd.5	|- ( ( ph /\ <. R , S , T >. = <. x , y , z >. ) -> Y = D )
	mpt3fvotd.6	|- F = ( x e. A , y e. B , z e. C |-> D )
Assertion	mpt3fvotd	|- ( ph -> ( F ` <. R , S , T >. ) = Y )

Proof

Step	Hyp	Ref	Expression
1		mpt3fvotd.1	|- ( ph -> R e. A )
2		mpt3fvotd.2	|- ( ph -> S e. B )
3		mpt3fvotd.3	|- ( ph -> T e. C )
4		mpt3fvotd.4	|- ( ph -> Y e. V )
5		mpt3fvotd.5	|- ( ( ph /\ <. R , S , T >. = <. x , y , z >. ) -> Y = D )
6		mpt3fvotd.6	|- F = ( x e. A , y e. B , z e. C |-> D )
7		otelxp	|- ( <. R , S , T >. e. ( ( A X. B ) X. C ) <-> ( R e. A /\ S e. B /\ T e. C ) )
8	1 2 3 7	syl3anbrc	|- ( ph -> <. R , S , T >. e. ( ( A X. B ) X. C ) )
9	8 4 5 6	mpt3fvd	|- ( ph -> ( F ` <. R , S , T >. ) = Y )