Theorem inindif

Description: See inundif . (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	1	orci	|- ( ( A i^i C ) C_ C \/ A C_ C )
3		inss	|- ( ( ( A i^i C ) C_ C \/ A C_ C ) -> ( ( A i^i C ) i^i A ) C_ C )
4	2 3	ax-mp	|- ( ( A i^i C ) i^i A ) C_ C
5		inssdif0	|- ( ( ( A i^i C ) i^i A ) C_ C <-> ( ( A i^i C ) i^i ( A \ C ) ) = (/) )
6	4 5	mpbi	|- ( ( A i^i C ) i^i ( A \ C ) ) = (/)