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 ( ( 𝐴𝑉𝐵𝑊 ) → ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ → { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ) )

Proof

Step Hyp Ref Expression
1 opthg ( ( 𝐴𝑉𝐵𝑊 ) → ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ↔ ( 𝐴 = 𝐶𝐵 = 𝐷 ) ) )
2 preq12 ( ( 𝐴 = 𝐶𝐵 = 𝐷 ) → { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } )
3 1 2 syl6bi ( ( 𝐴𝑉𝐵𝑊 ) → ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ → { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ) )