This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 |-