Theorem preq2

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

	Ref	Expression
Assertion	preq2	$$⊢A=B\to \left\{C,A\right\}=\left\{C,B\right\}$$

Proof

Step	Hyp	Ref	Expression
1		preq1	$$⊢A=B\to \left\{A,C\right\}=\left\{B,C\right\}$$
2		prcom	$$⊢\left\{C,A\right\}=\left\{A,C\right\}$$
3		prcom	$$⊢\left\{C,B\right\}=\left\{B,C\right\}$$
4	1 2 3	3eqtr4g	$$⊢A=B\to \left\{C,A\right\}=\left\{C,B\right\}$$