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