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
|- ( ph -> A e. V )
preq1b.b
|- ( ph -> B e. W )
Assertion preq2b
|- ( ph -> ( { C , A } = { C , B } <-> A = B ) )

Proof

Step Hyp Ref Expression
1 preq1b.a
 |-  ( ph -> A e. V )
2 preq1b.b
 |-  ( ph -> B e. W )
3 prcom
 |-  { C , A } = { A , C }
4 prcom
 |-  { C , B } = { B , C }
5 3 4 eqeq12i
 |-  ( { C , A } = { C , B } <-> { A , C } = { B , C } )
6 1 2 preq1b
 |-  ( ph -> ( { A , C } = { B , C } <-> A = B ) )
7 5 6 bitrid
 |-  ( ph -> ( { C , A } = { C , B } <-> A = B ) )