Metamath Proof Explorer


Theorem opprb

Description: Equality for unordered pairs corresponds to equality of unordered pairs with the same elements. (Contributed by AV, 9-Jul-2023)

Ref Expression
Assertion opprb A V B W C X D Y A B = C D A B = C D A B = D C

Proof

Step Hyp Ref Expression
1 preq12bg A V B W C X D Y A B = C D A = C B = D A = D B = C
2 opthg A V B W A B = C D A = C B = D
3 2 adantr A V B W C X D Y A B = C D A = C B = D
4 opthg A V B W A B = D C A = D B = C
5 4 adantr A V B W C X D Y A B = D C A = D B = C
6 3 5 orbi12d A V B W C X D Y A B = C D A B = D C A = C B = D A = D B = C
7 1 6 bitr4d A V B W C X D Y A B = C D A B = C D A B = D C