Theorem tpeq2

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

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

Proof

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