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