Metamath Proof Explorer

Theorem preq12b

Description: Equality relationship for two unordered pairs. (Contributed by NM, 17-Oct-1996)

Ref Expression
Hypotheses preqr1.a ⊢ A ∈ V
preqr1.b ⊢ B ∈ V
preq12b.c ⊢ C ∈ V
preq12b.d ⊢ D ∈ V
Assertion preq12b ⊢ A B = C D ↔ A = C ∧ B = D ∨ A = D ∧ B = C

Proof

Step Hyp Ref Expression
1 preqr1.a ⊢ A ∈ V
2 preqr1.b ⊢ B ∈ V
3 preq12b.c ⊢ C ∈ V
4 preq12b.d ⊢ D ∈ V
5 1 prid1 ⊢ A ∈ A B
6 eleq2 ⊢ A B = C D → A ∈ A B ↔ A ∈ C D
7 5 6 mpbii ⊢ A B = C D → A ∈ C D
8 1 elpr ⊢ A ∈ C D ↔ A = C ∨ A = D
9 7 8 sylib ⊢ A B = C D → A = C ∨ A = D
10 preq1 ⊢ A = C → A B = C B
11 10 eqeq1d ⊢ A = C → A B = C D ↔ C B = C D
12 2 4 preqr2 ⊢ C B = C D → B = D
13 11 12 syl6bi ⊢ A = C → A B = C D → B = D
14 13 com12 ⊢ A B = C D → A = C → B = D
15 14 ancld ⊢ A B = C D → A = C → A = C ∧ B = D
16 prcom ⊢ C D = D C
17 16 eqeq2i ⊢ A B = C D ↔ A B = D C
18 preq1 ⊢ A = D → A B = D B
19 18 eqeq1d ⊢ A = D → A B = D C ↔ D B = D C
20 2 3 preqr2 ⊢ D B = D C → B = C
21 19 20 syl6bi ⊢ A = D → A B = D C → B = C
22 21 com12 ⊢ A B = D C → A = D → B = C
23 17 22 sylbi ⊢ A B = C D → A = D → B = C
24 23 ancld ⊢ A B = C D → A = D → A = D ∧ B = C
25 15 24 orim12d ⊢ A B = C D → A = C ∨ A = D → A = C ∧ B = D ∨ A = D ∧ B = C
26 9 25 mpd ⊢ A B = C D → A = C ∧ B = D ∨ A = D ∧ B = C
27 preq12 ⊢ A = C ∧ B = D → A B = C D
28 preq12 ⊢ A = D ∧ B = C → A B = D C
29 prcom ⊢ D C = C D
30 28 29 eqtrdi ⊢ A = D ∧ B = C → A B = C D
31 27 30 jaoi ⊢ A = C ∧ B = D ∨ A = D ∧ B = C → A B = C D
32 26 31 impbii ⊢ A B = C D ↔ A = C ∧ B = D ∨ A = D ∧ B = C