Theorem preqr1

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

	Ref	Expression
Hypotheses	preqr1.a	$$⊢A\in \mathrm{V}$$
	preqr1.b	$$⊢B\in \mathrm{V}$$
Assertion	preqr1	$$⊢\left\{A,C\right\}=\left\{B,C\right\}\to A=B$$

Proof

Step	Hyp	Ref	Expression
1		preqr1.a	$$⊢A\in \mathrm{V}$$
2		preqr1.b	$$⊢B\in \mathrm{V}$$
3		id	$$⊢A\in \mathrm{V}\to A\in \mathrm{V}$$
4	2	a1i	$$⊢A\in \mathrm{V}\to B\in \mathrm{V}$$
5	3 4	preq1b	$$⊢A\in \mathrm{V}\to \left(\left\{A,C\right\}=\left\{B,C\right\}\leftrightarrow A=B\right)$$
6	1 5	ax-mp	$$⊢\left\{A,C\right\}=\left\{B,C\right\}\leftrightarrow A=B$$
7	6	biimpi	$$⊢\left\{A,C\right\}=\left\{B,C\right\}\to A=B$$