Theorem up1st2ndr

Description: Combine separated parts in the universal property predicate. (Contributed by Zhi Wang, 23-Oct-2025)

	Ref	Expression
Hypotheses	up1st2ndr.1	|- ( ph -> F e. ( D Func E ) )
	up1st2ndr.2	|- ( ph -> X ( <. ( 1st ` F ) , ( 2nd ` F ) >. ( D UP E ) W ) M )
Assertion	up1st2ndr	|- ( ph -> X ( F ( D UP E ) W ) M )

Proof

Step	Hyp	Ref	Expression
1		up1st2ndr.1	|- ( ph -> F e. ( D Func E ) )
2		up1st2ndr.2	|- ( ph -> X ( <. ( 1st ` F ) , ( 2nd ` F ) >. ( D UP E ) W ) M )
3		relfunc	|- Rel ( D Func E )
4		1st2nd	|- ( ( Rel ( D Func E ) /\ F e. ( D Func E ) ) -> F = <. ( 1st ` F ) , ( 2nd ` F ) >. )
5	3 1 4	sylancr	|- ( ph -> F = <. ( 1st ` F ) , ( 2nd ` F ) >. )
6	5	oveq1d	|- ( ph -> ( F ( D UP E ) W ) = ( <. ( 1st ` F ) , ( 2nd ` F ) >. ( D UP E ) W ) )
7	6	eqcomd	|- ( ph -> ( <. ( 1st ` F ) , ( 2nd ` F ) >. ( D UP E ) W ) = ( F ( D UP E ) W ) )
8	7 2	breqdi	|- ( ph -> X ( F ( D UP E ) W ) M )