Theorem preq2b

Description: Biconditional equality lemma for unordered pairs, deduction form. Two unordered pairs have the same first element iff the second elements are equal. (Contributed by AV, 18-Dec-2020)

	Ref	Expression
Hypotheses	preq1b.a	$$⊢\phi \to A\in V$$
	preq1b.b	$$⊢\phi \to B\in W$$
Assertion	preq2b	$$⊢\phi \to \left(\left\{C,A\right\}=\left\{C,B\right\}\leftrightarrow A=B\right)$$

Proof

Step	Hyp	Ref	Expression
1		preq1b.a	$$⊢\phi \to A\in V$$
2		preq1b.b	$$⊢\phi \to B\in W$$
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	preq1b	$$⊢\phi \to \left(\left\{A,C\right\}=\left\{B,C\right\}\leftrightarrow A=B\right)$$
7	5 6	bitrid	$$⊢\phi \to \left(\left\{C,A\right\}=\left\{C,B\right\}\leftrightarrow A=B\right)$$