Theorem preq2

Description: Equality theorem for unordered pairs. (Contributed by NM, 15-Jul-1993)

	Ref	Expression
Assertion	preq2	⊢ ( 𝐴 = 𝐵 → { 𝐶 , 𝐴 } = { 𝐶 , 𝐵 } )

Proof

Step	Hyp	Ref	Expression
1		preq1	⊢ ( 𝐴 = 𝐵 → { 𝐴 , 𝐶 } = { 𝐵 , 𝐶 } )
2		prcom	⊢ { 𝐶 , 𝐴 } = { 𝐴 , 𝐶 }
3		prcom	⊢ { 𝐶 , 𝐵 } = { 𝐵 , 𝐶 }
4	1 2 3	3eqtr4g	⊢ ( 𝐴 = 𝐵 → { 𝐶 , 𝐴 } = { 𝐶 , 𝐵 } )