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	⊢ 𝐴 ∈ V
	preqr1.b	⊢ 𝐵 ∈ V
Assertion	preqr2	⊢ ( { 𝐶 , 𝐴 } = { 𝐶 , 𝐵 } → 𝐴 = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		preqr1.a	⊢ 𝐴 ∈ V
2		preqr1.b	⊢ 𝐵 ∈ V
3		prcom	⊢ { 𝐶 , 𝐴 } = { 𝐴 , 𝐶 }
4		prcom	⊢ { 𝐶 , 𝐵 } = { 𝐵 , 𝐶 }
5	3 4	eqeq12i	⊢ ( { 𝐶 , 𝐴 } = { 𝐶 , 𝐵 } ↔ { 𝐴 , 𝐶 } = { 𝐵 , 𝐶 } )
6	1 2	preqr1	⊢ ( { 𝐴 , 𝐶 } = { 𝐵 , 𝐶 } → 𝐴 = 𝐵 )
7	5 6	sylbi	⊢ ( { 𝐶 , 𝐴 } = { 𝐶 , 𝐵 } → 𝐴 = 𝐵 )