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\in \mathrm{V}$$
	preqr1.b	$$⊢B\in \mathrm{V}$$
Assertion	preqr2	$$⊢\left\{C,A\right\}=\left\{C,B\right\}\to A=B$$

Proof

Step	Hyp	Ref	Expression
1		preqr1.a	$$⊢A\in \mathrm{V}$$
2		preqr1.b	$$⊢B\in \mathrm{V}$$
3		prcom	$$⊢\left\{C,A\right\}=\left\{A,C\right\}$$
4		prcom	$$⊢\left\{C,B\right\}=\left\{B,C\right\}$$
5	3 4	eqeq12i	$$⊢\left\{C,A\right\}=\left\{C,B\right\}\leftrightarrow \left\{A,C\right\}=\left\{B,C\right\}$$
6	1 2	preqr1	$$⊢\left\{A,C\right\}=\left\{B,C\right\}\to A=B$$
7	5 6	sylbi	$$⊢\left\{C,A\right\}=\left\{C,B\right\}\to A=B$$