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 ↔ A ∖ C ⊆ B

Proof

Step Hyp Ref Expression
1 uncom ⊢ B ∪ C = C ∪ B
2 1 sseq2i ⊢ A ⊆ B ∪ C ↔ A ⊆ C ∪ B
3 ssundif ⊢ A ⊆ B ∪ C ↔ A ∖ B ⊆ C
4 ssundif ⊢ A ⊆ C ∪ B ↔ A ∖ C ⊆ B
5 2 3 4 3bitr3i ⊢ A ∖ B ⊆ C ↔ A ∖ C ⊆ B