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