Metamath Proof Explorer


Theorem oppr

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

Ref Expression
Assertion oppr
|- ( ( A e. V /\ B e. W ) -> ( <. A , B >. = <. C , D >. -> { A , B } = { C , D } ) )

Proof

Step Hyp Ref Expression
1 opthg
 |-  ( ( A e. V /\ B e. W ) -> ( <. A , B >. = <. C , D >. <-> ( A = C /\ B = D ) ) )
2 preq12
 |-  ( ( A = C /\ B = D ) -> { A , B } = { C , D } )
3 1 2 syl6bi
 |-  ( ( A e. V /\ B e. W ) -> ( <. A , B >. = <. C , D >. -> { A , B } = { C , D } ) )