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

Metamath Proof Explorer

Theorem 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 ∈ V ∧ B ∈ W ∧ C ∈ X ∧ D ∈ Y → A B = C D ↔ A B = C D ∨ A B = D C

Proof

Step Hyp Ref Expression
1 preq12bg ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ X ∧ D ∈ Y → A B = C D ↔ A = C ∧ B = D ∨ A = D ∧ B = C
2 opthg ⊢ A ∈ V ∧ B ∈ W → A B = C D ↔ A = C ∧ B = D
3 2 adantr ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ X ∧ D ∈ Y → A B = C D ↔ A = C ∧ B = D
4 opthg ⊢ A ∈ V ∧ B ∈ W → A B = D C ↔ A = D ∧ B = C
5 4 adantr ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ X ∧ D ∈ Y → A B = D C ↔ A = D ∧ B = C
6 3 5 orbi12d ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ X ∧ D ∈ Y → A B = C D ∨ A B = D C ↔ A = C ∧ B = D ∨ A = D ∧ B = C
7 1 6 bitr4d ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ X ∧ D ∈ Y → A B = C D ↔ A B = C D ∨ A B = D C