Metamath Proof Explorer


Theorem preq1b

Description: Biconditional equality lemma for unordered pairs, deduction form. Two unordered pairs have the same second element iff the first elements are equal. (Contributed by AV, 18-Dec-2020)

Ref Expression
Hypotheses preq1b.a φ A V
preq1b.b φ B W
Assertion preq1b φ A C = B C A = B

Proof

Step Hyp Ref Expression
1 preq1b.a φ A V
2 preq1b.b φ B W
3 prid1g A V A A C
4 1 3 syl φ A A C
5 eleq2 A C = B C A A C A B C
6 4 5 syl5ibcom φ A C = B C A B C
7 elprg A V A B C A = B A = C
8 1 7 syl φ A B C A = B A = C
9 6 8 sylibd φ A C = B C A = B A = C
10 9 imp φ A C = B C A = B A = C
11 prid1g B W B B C
12 2 11 syl φ B B C
13 eleq2 A C = B C B A C B B C
14 12 13 syl5ibrcom φ A C = B C B A C
15 elprg B W B A C B = A B = C
16 2 15 syl φ B A C B = A B = C
17 14 16 sylibd φ A C = B C B = A B = C
18 17 imp φ A C = B C B = A B = C
19 eqcom A = B B = A
20 eqeq2 A = C B = A B = C
21 10 18 19 20 oplem1 φ A C = B C A = B
22 21 ex φ A C = B C A = B
23 preq1 A = B A C = B C
24 22 23 impbid1 φ A C = B C A = B