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 i^i B ) = (/) -> ( A \ B ) = A )

Proof

Step Hyp Ref Expression
1 difeq2 
 |-  ( ( A i^i B ) = (/) -> ( A \ ( A i^i B ) ) = ( A \ (/) ) )
2 difin 
 |-  ( A \ ( A i^i B ) ) = ( A \ B )
3 dif0 
 |-  ( A \ (/) ) = A
4 1 2 3 3eqtr3g 
 |-  ( ( A i^i B ) = (/) -> ( A \ B ) = A )