Theorem indifdir

Description: Distribute intersection over difference. (Contributed by Scott Fenton, 14-Apr-2011) (Revised by BTernaryTau, 14-Aug-2024)

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

Proof

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