Description: Equality for ordered pairs implies equality of unordered pairs with the same elements. (Contributed by AV, 9-Jul-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | oppr | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 〈 𝐴 , 𝐵 〉 = 〈 𝐶 , 𝐷 〉 → { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opthg | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 〈 𝐴 , 𝐵 〉 = 〈 𝐶 , 𝐷 〉 ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) ) | |
2 | preq12 | ⊢ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) → { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ) | |
3 | 1 2 | syl6bi | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 〈 𝐴 , 𝐵 〉 = 〈 𝐶 , 𝐷 〉 → { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ) ) |