Metamath Proof Explorer


Theorem bj-1uplth

Description: The characteristic property of monuples. Note that this holds without sethood hypotheses. (Contributed by BJ, 6-Apr-2019)

Ref Expression
Assertion bj-1uplth A = B A = B

Proof

Step Hyp Ref Expression
1 bj-pr1eq A = B pr1 A = pr1 B
2 bj-pr11val pr1 A = A
3 bj-pr11val pr1 B = B
4 1 2 3 3eqtr3g A = B A = B
5 bj-1upleq A = B A = B
6 4 5 impbii A = B A = B