Theorem indif1

Description: Bring an intersection in and out of a class difference. (Contributed by Mario Carneiro, 15-May-2015)

	Ref	Expression
Assertion	indif1	|- ( ( A \ C ) i^i B ) = ( ( A i^i B ) \ C )

Proof

Step	Hyp	Ref	Expression
1		indif2	|- ( B i^i ( A \ C ) ) = ( ( B i^i A ) \ C )
2		incom	|- ( B i^i ( A \ C ) ) = ( ( A \ C ) i^i B )
3		incom	|- ( B i^i A ) = ( A i^i B )
4	3	difeq1i	|- ( ( B i^i A ) \ C ) = ( ( A i^i B ) \ C )
5	1 2 4	3eqtr3i	|- ( ( A \ C ) i^i B ) = ( ( A i^i B ) \ C )