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⦆\leftrightarrow \left(A=C\wedge B=D\right)$$

Proof

Step	Hyp	Ref	Expression
1		bj-pr1eq	$$⊢⦅A,B⦆=⦅C,D⦆\to 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⦆\to A=C$$
5		bj-pr2eq	$$⊢⦅A,B⦆=⦅C,D⦆\to 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⦆\to B=D$$
9	4 8	jca	$$⊢⦅A,B⦆=⦅C,D⦆\to \left(A=C\wedge B=D\right)$$
10		bj-2upleq	$$⊢A=C\to \left(B=D\to ⦅A,B⦆=⦅C,D⦆\right)$$
11	10	imp	$$⊢\left(A=C\wedge B=D\right)\to ⦅A,B⦆=⦅C,D⦆$$
12	9 11	impbii	$$⊢⦅A,B⦆=⦅C,D⦆\leftrightarrow \left(A=C\wedge B=D\right)$$