Metamath Proof Explorer


Theorem disjdifr

Description: A class and its relative complement are disjoint. Commuted form of disjdif . (Contributed by Thierry Arnoux, 29-Nov-2023)

Ref Expression
Assertion disjdifr ⊢ B ∖ A ∩ A = ∅

Proof

Step Hyp Ref Expression
1 disjdif ⊢ A ∩ B ∖ A = ∅
2 1 ineqcomi ⊢ B ∖ A ∩ A = ∅