Metamath Proof Explorer

Theorem sscon34b

Description: Relative complementation reverses inclusion of subclasses. Relativized version of complss . (Contributed by RP, 3-Jun-2021)

Ref Expression
Assertion sscon34b ⊢ A ⊆ C ∧ B ⊆ C → A ⊆ B ↔ C ∖ B ⊆ C ∖ A

Proof

Step Hyp Ref Expression
1 sscon ⊢ A ⊆ B → C ∖ B ⊆ C ∖ A
2 sscon ⊢ C ∖ B ⊆ C ∖ A → C ∖ C ∖ A ⊆ C ∖ C ∖ B
3 dfss4 ⊢ A ⊆ C ↔ C ∖ C ∖ A = A
4 3 biimpi ⊢ A ⊆ C → C ∖ C ∖ A = A
5 4 adantr ⊢ A ⊆ C ∧ B ⊆ C → C ∖ C ∖ A = A
6 dfss4 ⊢ B ⊆ C ↔ C ∖ C ∖ B = B
7 6 biimpi ⊢ B ⊆ C → C ∖ C ∖ B = B
8 7 adantl ⊢ A ⊆ C ∧ B ⊆ C → C ∖ C ∖ B = B
9 5 8 sseq12d ⊢ A ⊆ C ∧ B ⊆ C → C ∖ C ∖ A ⊆ C ∖ C ∖ B ↔ A ⊆ B
10 2 9 syl5ib ⊢ A ⊆ C ∧ B ⊆ C → C ∖ B ⊆ C ∖ A → A ⊆ B
11 1 10 impbid2 ⊢ A ⊆ C ∧ B ⊆ C → A ⊆ B ↔ C ∖ B ⊆ C ∖ A