Metamath Proof Explorer

Theorem disjdif2

Description: The difference of a class and a class disjoint from it is the original class. (Contributed by BJ, 21-Apr-2019)

Ref Expression
Assertion disjdif2 A B = A B = A


Step Hyp Ref Expression
1 difeq2 A B = A A B = A
2 difin A A B = A B
3 dif0 A = A
4 1 2 3 3eqtr3g A B = A B = A