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 -> { A , B , C } = { A , B } )

Proof

Step	Hyp	Ref	Expression
1		tpeq3	|- ( C = B -> { A , B , C } = { A , B , B } )
2	1	eqcoms	|- ( B = C -> { A , B , C } = { A , B , B } )
3		tpidm23	|- { A , B , B } = { A , B }
4	2 3	eqtrdi	|- ( B = C -> { A , B , C } = { A , B } )