Theorem indifcom

Description: Commutation law for intersection and difference. (Contributed by Scott Fenton, 18-Feb-2013)

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

Proof

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