Metamath Proof Explorer

Theorem ssconb

Description: Contraposition law for subsets. (Contributed by NM, 22-Mar-1998)

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

Proof

Step Hyp Ref Expression
1 ssel ⊢ A ⊆ C → x ∈ A → x ∈ C
2 ssel ⊢ B ⊆ C → x ∈ B → x ∈ C
3 pm5.1 ⊢ x ∈ A → x ∈ C ∧ x ∈ B → x ∈ C → x ∈ A → x ∈ C ↔ x ∈ B → x ∈ C
4 1 2 3 syl2an ⊢ A ⊆ C ∧ B ⊆ C → x ∈ A → x ∈ C ↔ x ∈ B → x ∈ C
5 con2b ⊢ x ∈ A → ¬ x ∈ B ↔ x ∈ B → ¬ x ∈ A
6 5 a1i ⊢ A ⊆ C ∧ B ⊆ C → x ∈ A → ¬ x ∈ B ↔ x ∈ B → ¬ x ∈ A
7 4 6 anbi12d ⊢ A ⊆ C ∧ B ⊆ C → x ∈ A → x ∈ C ∧ x ∈ A → ¬ x ∈ B ↔ x ∈ B → x ∈ C ∧ x ∈ B → ¬ x ∈ A
8 jcab ⊢ x ∈ A → x ∈ C ∧ ¬ x ∈ B ↔ x ∈ A → x ∈ C ∧ x ∈ A → ¬ x ∈ B
9 jcab ⊢ x ∈ B → x ∈ C ∧ ¬ x ∈ A ↔ x ∈ B → x ∈ C ∧ x ∈ B → ¬ x ∈ A
10 7 8 9 3bitr4g ⊢ A ⊆ C ∧ B ⊆ C → x ∈ A → x ∈ C ∧ ¬ x ∈ B ↔ x ∈ B → x ∈ C ∧ ¬ x ∈ A
11 eldif ⊢ x ∈ C ∖ B ↔ x ∈ C ∧ ¬ x ∈ B
12 11 imbi2i ⊢ x ∈ A → x ∈ C ∖ B ↔ x ∈ A → x ∈ C ∧ ¬ x ∈ B
13 eldif ⊢ x ∈ C ∖ A ↔ x ∈ C ∧ ¬ x ∈ A
14 13 imbi2i ⊢ x ∈ B → x ∈ C ∖ A ↔ x ∈ B → x ∈ C ∧ ¬ x ∈ A
15 10 12 14 3bitr4g ⊢ A ⊆ C ∧ B ⊆ C → x ∈ A → x ∈ C ∖ B ↔ x ∈ B → x ∈ C ∖ A
16 15 albidv ⊢ A ⊆ C ∧ B ⊆ C → ∀ x x ∈ A → x ∈ C ∖ B ↔ ∀ x x ∈ B → x ∈ C ∖ A
17 df-ss ⊢ A ⊆ C ∖ B ↔ ∀ x x ∈ A → x ∈ C ∖ B
18 df-ss ⊢ B ⊆ C ∖ A ↔ ∀ x x ∈ B → x ∈ C ∖ A
19 16 17 18 3bitr4g ⊢ A ⊆ C ∧ B ⊆ C → A ⊆ C ∖ B ↔ B ⊆ C ∖ A