Theorem preqr1g

Description: Reverse equality lemma for unordered pairs. If two unordered pairs have the same second element, the first elements are equal. Closed form of preqr1 . (Contributed by AV, 29-Jan-2021) (Revised by AV, 18-Sep-2021)

	Ref	Expression
Assertion	preqr1g	$$⊢\left(A\in V\wedge B\in W\right)\to \left(\left\{A,C\right\}=\left\{B,C\right\}\to A=B\right)$$

Proof

Step	Hyp	Ref	Expression
1		simpl	$$⊢\left(A\in V\wedge B\in W\right)\to A\in V$$
2		simpr	$$⊢\left(A\in V\wedge B\in W\right)\to B\in W$$
3	1 2	preq1b	$$⊢\left(A\in V\wedge B\in W\right)\to \left(\left\{A,C\right\}=\left\{B,C\right\}\leftrightarrow A=B\right)$$
4	3	biimpd	$$⊢\left(A\in V\wedge B\in W\right)\to \left(\left\{A,C\right\}=\left\{B,C\right\}\to A=B\right)$$