Theorem qdass

Description: Two ways to write an unordered quadruple. (Contributed by Mario Carneiro, 5-Jan-2016)

	Ref	Expression
Assertion	qdass	|- ( { A , B } u. { C , D } ) = ( { A , B , C } u. { D } )

Proof

Step	Hyp	Ref	Expression
1		unass	|- ( ( { A , B } u. { C } ) u. { D } ) = ( { A , B } u. ( { C } u. { D } ) )
2		df-tp	|- { A , B , C } = ( { A , B } u. { C } )
3	2	uneq1i	|- ( { A , B , C } u. { D } ) = ( ( { A , B } u. { C } ) u. { D } )
4		df-pr	|- { C , D } = ( { C } u. { D } )
5	4	uneq2i	|- ( { A , B } u. { C , D } ) = ( { A , B } u. ( { C } u. { D } ) )
6	1 3 5	3eqtr4ri	|- ( { A , B } u. { C , D } ) = ( { A , B , C } u. { D } )