Theorem inindif

Description: The intersection and class difference of a class with another class are disjoint. With inundif , this shows that such intersection and class difference partition the class A . (Contributed by Thierry Arnoux, 13-Sep-2017)

	Ref	Expression
Assertion	inindif	|- ( ( A i^i C ) i^i ( A \ C ) ) = (/)

Proof

Step	Hyp	Ref	Expression
1		inss2	|- ( A i^i C ) C_ C
2		ssinss1	|- ( ( A i^i C ) C_ C -> ( ( A i^i C ) i^i A ) C_ C )
3	1 2	ax-mp	|- ( ( A i^i C ) i^i A ) C_ C
4		inssdif0	|- ( ( ( A i^i C ) i^i A ) C_ C <-> ( ( A i^i C ) i^i ( A \ C ) ) = (/) )
5	3 4	mpbi	|- ( ( A i^i C ) i^i ( A \ C ) ) = (/)