Theorem tppreq3

Description: An unordered triple is an unordered pair if one of its elements is identical with another element. (Contributed by Alexander van der Vekens, 6-Oct-2017)

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

Proof

Step	Hyp	Ref	Expression
1		tpeq3	$$⊢C=B\to \left\{A,B,C\right\}=\left\{A,B,B\right\}$$
2	1	eqcoms	$$⊢B=C\to \left\{A,B,C\right\}=\left\{A,B,B\right\}$$
3		tpidm23	$$⊢\left\{A,B,B\right\}=\left\{A,B\right\}$$
4	2 3	eqtrdi	$$⊢B=C\to \left\{A,B,C\right\}=\left\{A,B\right\}$$