Theorem tpeq1

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

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

Proof

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