Theorem up1st2nd2

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

	Ref	Expression
Hypothesis	up1st2nd2.1	No typesetting found for |- ( ph -> X e. ( F ( D UP E ) W ) ) with typecode |-
Assertion	up1st2nd2	Could not format assertion : No typesetting found for |- ( ph -> ( 1st ` X ) ( F ( D UP E ) W ) ( 2nd ` X ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		up1st2nd2.1	Could not format ( ph -> X e. ( F ( D UP E ) W ) ) : No typesetting found for |- ( ph -> X e. ( F ( D UP E ) W ) ) with typecode |-
2		relup	Could not format Rel ( F ( D UP E ) W ) : No typesetting found for |- Rel ( F ( D UP E ) W ) with typecode |-
3		1st2ndbr	Could not format ( ( Rel ( F ( D UP E ) W ) /\ X e. ( F ( D UP E ) W ) ) -> ( 1st ` X ) ( F ( D UP E ) W ) ( 2nd ` X ) ) : No typesetting found for |- ( ( Rel ( F ( D UP E ) W ) /\ X e. ( F ( D UP E ) W ) ) -> ( 1st ` X ) ( F ( D UP E ) W ) ( 2nd ` X ) ) with typecode |-
4	2 1 3	sylancr	Could not format ( ph -> ( 1st ` X ) ( F ( D UP E ) W ) ( 2nd ` X ) ) : No typesetting found for |- ( ph -> ( 1st ` X ) ( F ( D UP E ) W ) ( 2nd ` X ) ) with typecode |-