Theorem difpr

Description: Removing two elements as pair of elements corresponds to removing each of the two elements as singletons. (Contributed by Alexander van der Vekens, 13-Jul-2018)

	Ref	Expression
Assertion	difpr	|- ( A \ { B , C } ) = ( ( A \ { B } ) \ { C } )

Proof

Step	Hyp	Ref	Expression
1		df-pr	|- { B , C } = ( { B } u. { C } )
2	1	difeq2i	|- ( A \ { B , C } ) = ( A \ ( { B } u. { C } ) )
3		difun1	|- ( A \ ( { B } u. { C } ) ) = ( ( A \ { B } ) \ { C } )
4	2 3	eqtri	|- ( A \ { B , C } ) = ( ( A \ { B } ) \ { C } )