This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) -> ( { A , B } = { C , D } <-> ( <. A , B >. = <. C , D >. \/ <. A , B >. = <. D , C >. ) ) )

Proof

Step Hyp Ref Expression
1 preq12bg 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) -> ( { A , B } = { C , D } <-> ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) ) )
2 opthg 
 |-  ( ( A e. V /\ B e. W ) -> ( <. A , B >. = <. C , D >. <-> ( A = C /\ B = D ) ) )
3 2 adantr 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) -> ( <. A , B >. = <. C , D >. <-> ( A = C /\ B = D ) ) )
4 opthg 
 |-  ( ( A e. V /\ B e. W ) -> ( <. A , B >. = <. D , C >. <-> ( A = D /\ B = C ) ) )
5 4 adantr 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) -> ( <. A , B >. = <. D , C >. <-> ( A = D /\ B = C ) ) )
6 3 5 orbi12d 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) -> ( ( <. A , B >. = <. C , D >. \/ <. A , B >. = <. D , C >. ) <-> ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) ) )
7 1 6 bitr4d 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) -> ( { A , B } = { C , D } <-> ( <. A , B >. = <. C , D >. \/ <. A , B >. = <. D , C >. ) ) )