Metamath Proof Explorer


Theorem bj-2uplth

Description: The characteristic property of couples. Note that this holds without sethood hypotheses (compare opth ). (Contributed by BJ, 6-Oct-2018)

Ref Expression
Assertion bj-2uplth A B = C D A = C B = D

Proof

Step Hyp Ref Expression
1 bj-pr1eq A B = C D pr1 A B = pr1 C D
2 bj-pr21val pr1 A B = A
3 bj-pr21val pr1 C D = C
4 1 2 3 3eqtr3g A B = C D A = C
5 bj-pr2eq A B = C D pr2 A B = pr2 C D
6 bj-pr22val pr2 A B = B
7 bj-pr22val pr2 C D = D
8 5 6 7 3eqtr3g A B = C D B = D
9 4 8 jca A B = C D A = C B = D
10 bj-2upleq A = C B = D A B = C D
11 10 imp A = C B = D A B = C D
12 9 11 impbii A B = C D A = C B = D