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 ( ( 𝐴𝐶 ) ∩ ( 𝐴𝐶 ) ) = ∅

Proof

Step Hyp Ref Expression
1 inss2 ( 𝐴𝐶 ) ⊆ 𝐶
2 ssinss1 ( ( 𝐴𝐶 ) ⊆ 𝐶 → ( ( 𝐴𝐶 ) ∩ 𝐴 ) ⊆ 𝐶 )
3 1 2 ax-mp ( ( 𝐴𝐶 ) ∩ 𝐴 ) ⊆ 𝐶
4 inssdif0 ( ( ( 𝐴𝐶 ) ∩ 𝐴 ) ⊆ 𝐶 ↔ ( ( 𝐴𝐶 ) ∩ ( 𝐴𝐶 ) ) = ∅ )
5 3 4 mpbi ( ( 𝐴𝐶 ) ∩ ( 𝐴𝐶 ) ) = ∅