Metamath Proof Explorer

Theorem undif5

Description: An equality involving class union and class difference. (Contributed by Thierry Arnoux, 26-Jun-2024)

Ref Expression
Assertion undif5 
|- ( ( A i^i B ) = (/) -> ( ( A u. B ) \ B ) = A )

Proof

Step Hyp Ref Expression
1 difun2 
 |-  ( ( A u. B ) \ B ) = ( A \ B )
2 disjdif2 
 |-  ( ( A i^i B ) = (/) -> ( A \ B ) = A )
3 1 2 syl5eq 
 |-  ( ( A i^i B ) = (/) -> ( ( A u. B ) \ B ) = A )