Metamath Proof Explorer

Theorem ssundif

Description: A condition equivalent to inclusion in the union of two classes. (Contributed by NM, 26-Mar-2007)

Ref Expression
Assertion ssundif ⊢ A ⊆ B ∪ C ↔ A ∖ B ⊆ C

Proof

Step Hyp Ref Expression
1 pm5.6 ⊢ x ∈ A ∧ ¬ x ∈ B → x ∈ C ↔ x ∈ A → x ∈ B ∨ x ∈ C
2 eldif ⊢ x ∈ A ∖ B ↔ x ∈ A ∧ ¬ x ∈ B
3 2 imbi1i ⊢ x ∈ A ∖ B → x ∈ C ↔ x ∈ A ∧ ¬ x ∈ B → x ∈ C
4 elun ⊢ x ∈ B ∪ C ↔ x ∈ B ∨ x ∈ C
5 4 imbi2i ⊢ x ∈ A → x ∈ B ∪ C ↔ x ∈ A → x ∈ B ∨ x ∈ C
6 1 3 5 3bitr4ri ⊢ x ∈ A → x ∈ B ∪ C ↔ x ∈ A ∖ B → x ∈ C
7 6 albii ⊢ ∀ x x ∈ A → x ∈ B ∪ C ↔ ∀ x x ∈ A ∖ B → x ∈ C
8 df-ss ⊢ A ⊆ B ∪ C ↔ ∀ x x ∈ A → x ∈ B ∪ C
9 df-ss ⊢ A ∖ B ⊆ C ↔ ∀ x x ∈ A ∖ B → x ∈ C
10 7 8 9 3bitr4i ⊢ A ⊆ B ∪ C ↔ A ∖ B ⊆ C