opprb

Description: Equality for unordered pairs corresponds to equality of unordered pairs with the same elements. (Contributed by AV, 9-Jul-2023)

		Ref	Expression
	Assertion	opprb	$⊢ ((A \in V \land B \in W) \land (C \in X \land D \in Y)) \to (\{A, B\} = \{C, D\} \leftrightarrow (⟨A, B⟩ = ⟨C, D⟩ \lor ⟨A, B⟩ = ⟨D, C⟩))$

Step	Hyp	Ref	Expression
1		preq12bg	$⊢ ((A \in V \land B \in W) \land (C \in X \land D \in Y)) \to (\{A, B\} = \{C, D\} \leftrightarrow ((A = C \land B = D) \lor (A = D \land B = C)))$
2		opthg	$⊢ (A \in V \land B \in W) \to (⟨A, B⟩ = ⟨C, D⟩ \leftrightarrow (A = C \land B = D))$
3	2	adantr	$⊢ ((A \in V \land B \in W) \land (C \in X \land D \in Y)) \to (⟨A, B⟩ = ⟨C, D⟩ \leftrightarrow (A = C \land B = D))$
4		opthg	$⊢ (A \in V \land B \in W) \to (⟨A, B⟩ = ⟨D, C⟩ \leftrightarrow (A = D \land B = C))$
5	4	adantr	$⊢ ((A \in V \land B \in W) \land (C \in X \land D \in Y)) \to (⟨A, B⟩ = ⟨D, C⟩ \leftrightarrow (A = D \land B = C))$
6	3 5	orbi12d	$⊢ ((A \in V \land B \in W) \land (C \in X \land D \in Y)) \to ((⟨A, B⟩ = ⟨C, D⟩ \lor ⟨A, B⟩ = ⟨D, C⟩) \leftrightarrow ((A = C \land B = D) \lor (A = D \land B = C)))$
7	1 6	bitr4d	$⊢ ((A \in V \land B \in W) \land (C \in X \land D \in Y)) \to (\{A, B\} = \{C, D\} \leftrightarrow (⟨A, B⟩ = ⟨C, D⟩ \lor ⟨A, B⟩ = ⟨D, C⟩))$

Metamath Proof Explorer