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	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	preq1b.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
Assertion	preq2b	⊢ ( 𝜑 → ( { 𝐶 , 𝐴 } = { 𝐶 , 𝐵 } ↔ 𝐴 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		preq1b.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		preq1b.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3		prcom	⊢ { 𝐶 , 𝐴 } = { 𝐴 , 𝐶 }
4		prcom	⊢ { 𝐶 , 𝐵 } = { 𝐵 , 𝐶 }
5	3 4	eqeq12i	⊢ ( { 𝐶 , 𝐴 } = { 𝐶 , 𝐵 } ↔ { 𝐴 , 𝐶 } = { 𝐵 , 𝐶 } )
6	1 2	preq1b	⊢ ( 𝜑 → ( { 𝐴 , 𝐶 } = { 𝐵 , 𝐶 } ↔ 𝐴 = 𝐵 ) )
7	5 6	bitrid	⊢ ( 𝜑 → ( { 𝐶 , 𝐴 } = { 𝐶 , 𝐵 } ↔ 𝐴 = 𝐵 ) )