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	$$⊢\left(A\in V\wedge B\in W\right)\to \left(⟨A,B⟩=⟨C,D⟩\to \left\{A,B\right\}=\left\{C,D\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		opthg	$$⊢\left(A\in V\wedge B\in W\right)\to \left(⟨A,B⟩=⟨C,D⟩\leftrightarrow \left(A=C\wedge B=D\right)\right)$$
2		preq12	$$⊢\left(A=C\wedge B=D\right)\to \left\{A,B\right\}=\left\{C,D\right\}$$
3	1 2	biimtrdi	$$⊢\left(A\in V\wedge B\in W\right)\to \left(⟨A,B⟩=⟨C,D⟩\to \left\{A,B\right\}=\left\{C,D\right\}\right)$$