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 C A C =

Proof

Step Hyp Ref Expression
1 inss2 A C C
2 ssinss1 A C C A C A C
3 1 2 ax-mp A C A C
4 inssdif0 A C A C A C A C =
5 3 4 mpbi A C A C =