Metamath Proof Explorer


Theorem preqr2

Description: Reverse equality lemma for unordered pairs. If two unordered pairs have the same first element, the second elements are equal. (Contributed by NM, 15-Jul-1993)

Ref Expression
Hypotheses preqr1.a
|- A e. _V
preqr1.b
|- B e. _V
Assertion preqr2
|- ( { C , A } = { C , B } -> A = B )

Proof

Step Hyp Ref Expression
1 preqr1.a
 |-  A e. _V
2 preqr1.b
 |-  B e. _V
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 preqr1
 |-  ( { A , C } = { B , C } -> A = B )
7 5 6 sylbi
 |-  ( { C , A } = { C , B } -> A = B )