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→AB=CD↔A∈CD∧B∈CD

Proof

Step Hyp Ref Expression
1 preq12nebg ⊢A∈V∧B∈W∧A≠B→AB=CD↔A=C∧B=D∨A=D∧B=C
2 prid1g ⊢A∈V→A∈AD
3 2 3ad2ant1 ⊢A∈V∧B∈W∧A≠B→A∈AD
4 3 adantr ⊢A∈V∧B∈W∧A≠B∧A=C→A∈AD
5 preq1 ⊢A=C→AD=CD
6 5 adantl ⊢A∈V∧B∈W∧A≠B∧A=C→AD=CD
7 4 6 eleqtrd ⊢A∈V∧B∈W∧A≠B∧A=C→A∈CD
8 7 ex ⊢A∈V∧B∈W∧A≠B→A=C→A∈CD
9 prid2g ⊢B∈W→B∈CB
10 9 3ad2ant2 ⊢A∈V∧B∈W∧A≠B→B∈CB
11 preq2 ⊢B=D→CB=CD
12 11 eleq2d ⊢B=D→B∈CB↔B∈CD
13 10 12 syl5ibcom ⊢A∈V∧B∈W∧A≠B→B=D→B∈CD
14 8 13 anim12d ⊢A∈V∧B∈W∧A≠B→A=C∧B=D→A∈CD∧B∈CD
15 prid2g ⊢A∈V→A∈CA
16 15 3ad2ant1 ⊢A∈V∧B∈W∧A≠B→A∈CA
17 preq2 ⊢A=D→CA=CD
18 17 eleq2d ⊢A=D→A∈CA↔A∈CD
19 16 18 syl5ibcom ⊢A∈V∧B∈W∧A≠B→A=D→A∈CD
20 prid1g ⊢B∈W→B∈BD
21 20 3ad2ant2 ⊢A∈V∧B∈W∧A≠B→B∈BD
22 preq1 ⊢B=C→BD=CD
23 22 eleq2d ⊢B=C→B∈BD↔B∈CD
24 21 23 syl5ibcom ⊢A∈V∧B∈W∧A≠B→B=C→B∈CD
25 19 24 anim12d ⊢A∈V∧B∈W∧A≠B→A=D∧B=C→A∈CD∧B∈CD
26 14 25 jaod ⊢A∈V∧B∈W∧A≠B→A=C∧B=D∨A=D∧B=C→A∈CD∧B∈CD
27 elprg ⊢A∈V→A∈CD↔A=C∨A=D
28 27 3ad2ant1 ⊢A∈V∧B∈W∧A≠B→A∈CD↔A=C∨A=D
29 elprg ⊢B∈W→B∈CD↔B=C∨B=D
30 29 3ad2ant2 ⊢A∈V∧B∈W∧A≠B→B∈CD↔B=C∨B=D
31 28 30 anbi12d ⊢A∈V∧B∈W∧A≠B→A∈CD∧B∈CD↔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∈CD∧B∈CD→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∈CD∧B∈CD
46 1 45 bitrd ⊢A∈V∧B∈W∧A≠B→AB=CD↔A∈CD∧B∈CD