Metamath Proof Explorer

Theorem prel12g

Description: Equality of two unordered pairs. (Contributed by NM, 17-Oct-1996) (Revised by AV, 9-Dec-2018) (Revised by AV, 12-Jun-2022)

Ref Expression
Assertion prel12g ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B → A B = C D ↔ A ∈ C D ∧ B ∈ C D

Proof

Step Hyp Ref Expression
1 preq12nebg ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B → A B = C D ↔ A = C ∧ B = D ∨ A = D ∧ B = C
2 prid1g ⊢ A ∈ V → A ∈ A D
3 2 3ad2ant1 ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B → A ∈ A D
4 3 adantr ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B ∧ A = C → A ∈ A D
5 preq1 ⊢ A = C → A D = C D
6 5 adantl ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B ∧ A = C → A D = C D
7 4 6 eleqtrd ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B ∧ A = C → A ∈ C D
8 7 ex ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B → A = C → A ∈ C D
9 prid2g ⊢ B ∈ W → B ∈ C B
10 9 3ad2ant2 ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B → B ∈ C B
11 preq2 ⊢ B = D → C B = C D
12 11 eleq2d ⊢ B = D → B ∈ C B ↔ B ∈ C D
13 10 12 syl5ibcom ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B → B = D → B ∈ C D
14 8 13 anim12d ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B → A = C ∧ B = D → A ∈ C D ∧ B ∈ C D
15 prid2g ⊢ A ∈ V → A ∈ C A
16 15 3ad2ant1 ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B → A ∈ C A
17 preq2 ⊢ A = D → C A = C D
18 17 eleq2d ⊢ A = D → A ∈ C A ↔ A ∈ C D
19 16 18 syl5ibcom ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B → A = D → A ∈ C D
20 prid1g ⊢ B ∈ W → B ∈ B D
21 20 3ad2ant2 ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B → B ∈ B D
22 preq1 ⊢ B = C → B D = C D
23 22 eleq2d ⊢ B = C → B ∈ B D ↔ B ∈ C D
24 21 23 syl5ibcom ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B → B = C → B ∈ C D
25 19 24 anim12d ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B → A = D ∧ B = C → A ∈ C D ∧ B ∈ C D
26 14 25 jaod ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B → A = C ∧ B = D ∨ A = D ∧ B = C → A ∈ C D ∧ B ∈ C D
27 elprg ⊢ A ∈ V → A ∈ C D ↔ A = C ∨ A = D
28 27 3ad2ant1 ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B → A ∈ C D ↔ A = C ∨ A = D
29 elprg ⊢ B ∈ W → B ∈ C D ↔ B = C ∨ B = D
30 29 3ad2ant2 ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B → B ∈ C D ↔ B = C ∨ B = D
31 28 30 anbi12d ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B → A ∈ C D ∧ B ∈ C D ↔ A = C ∨ A = D ∧ B = C ∨ B = D
32 eqtr3 ⊢ A = C ∧ B = C → A = B
33 eqneqall ⊢ A = B → A ≠ B → A = C ∧ B = D ∨ A = D ∧ B = C
34 32 33 syl ⊢ A = C ∧ B = C → A ≠ B → A = C ∧ B = D ∨ A = D ∧ B = C
35 olc ⊢ A = D ∧ B = C → A = C ∧ B = D ∨ A = D ∧ B = C
36 35 a1d ⊢ A = D ∧ B = C → A ≠ B → A = C ∧ B = D ∨ A = D ∧ B = C
37 orc ⊢ A = C ∧ B = D → A = C ∧ B = D ∨ A = D ∧ B = C
38 37 a1d ⊢ A = C ∧ B = D → A ≠ B → A = C ∧ B = D ∨ A = D ∧ B = C
39 eqtr3 ⊢ A = D ∧ B = D → A = B
40 39 33 syl ⊢ A = D ∧ B = D → A ≠ B → A = C ∧ B = D ∨ A = D ∧ B = C
41 34 36 38 40 ccase ⊢ A = C ∨ A = D ∧ B = C ∨ B = D → A ≠ B → A = C ∧ B = D ∨ A = D ∧ B = C
42 41 com12 ⊢ A ≠ B → A = C ∨ A = D ∧ B = C ∨ B = D → A = C ∧ B = D ∨ A = D ∧ B = C
43 42 3ad2ant3 ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B → A = C ∨ A = D ∧ B = C ∨ B = D → A = C ∧ B = D ∨ A = D ∧ B = C
44 31 43 sylbid ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B → A ∈ C D ∧ B ∈ C D → A = C ∧ B = D ∨ A = D ∧ B = C
45 26 44 impbid ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B → A = C ∧ B = D ∨ A = D ∧ B = C ↔ A ∈ C D ∧ B ∈ C D
46 1 45 bitrd ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B → A B = C D ↔ A ∈ C D ∧ B ∈ C D