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 )