Metamath Proof Explorer

Theorem difcom

Description: Swap the arguments of a class difference. (Contributed by NM, 29-Mar-2007)

Ref Expression
Assertion difcom 
|- ( ( A \ B ) C_ C <-> ( A \ C ) C_ B )

Proof

Step Hyp Ref Expression
1 uncom 
 |-  ( B u. C ) = ( C u. B )
2 1 sseq2i 
 |-  ( A C_ ( B u. C ) <-> A C_ ( C u. B ) )
3 ssundif 
 |-  ( A C_ ( B u. C ) <-> ( A \ B ) C_ C )
4 ssundif 
 |-  ( A C_ ( C u. B ) <-> ( A \ C ) C_ B )
5 2 3 4 3bitr3i 
 |-  ( ( A \ B ) C_ C <-> ( A \ C ) C_ B )