Metamath Proof Explorer


Theorem preq2b

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

Ref Expression
Hypotheses preq1b.a φAV
preq1b.b φBW
Assertion preq2b φCA=CBA=B

Proof

Step Hyp Ref Expression
1 preq1b.a φAV
2 preq1b.b φBW
3 prcom CA=AC
4 prcom CB=BC
5 3 4 eqeq12i CA=CBAC=BC
6 1 2 preq1b φAC=BCA=B
7 5 6 bitrid φCA=CBA=B