Metamath Proof Explorer

Theorem disjdifr

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

Ref Expression
Assertion disjdifr 
|- ( ( B \ A ) i^i A ) = (/)

Proof

Step Hyp Ref Expression
1 incom 
 |-  ( A i^i ( B \ A ) ) = ( ( B \ A ) i^i A )
2 disjdif 
 |-  ( A i^i ( B \ A ) ) = (/)
3 1 2 eqtr3i 
 |-  ( ( B \ A ) i^i A ) = (/)