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