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 )