This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

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