Metamath Proof Explorer

Theorem disjdif

Description: A class and its relative complement are disjoint. Theorem 38 of Suppes p. 29. (Contributed by NM, 24-Mar-1998)

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

Proof

Step Hyp Ref Expression
1 inss1 
 |-  ( A i^i B ) C_ A
2 inssdif0 
 |-  ( ( A i^i B ) C_ A <-> ( A i^i ( B \ A ) ) = (/) )
3 1 2 mpbi 
 |-  ( A i^i ( B \ A ) ) = (/)