Theorem tpeq3

Description: Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011)

	Ref	Expression
Assertion	tpeq3	|- ( A = B -> { C , D , A } = { C , D , B } )

Proof

Step	Hyp	Ref	Expression
1		sneq	|- ( A = B -> { A } = { B } )
2	1	uneq2d	|- ( A = B -> ( { C , D } u. { A } ) = ( { C , D } u. { B } ) )
3		df-tp	|- { C , D , A } = ( { C , D } u. { A } )
4		df-tp	|- { C , D , B } = ( { C , D } u. { B } )
5	2 3 4	3eqtr4g	|- ( A = B -> { C , D , A } = { C , D , B } )