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

Proof

Step Hyp Ref Expression
1 inss1 A B A
2 inssdif0 A B A A B A =
3 1 2 mpbi A B A =