Metamath Proof Explorer


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 ) ) = (/)