Metamath Proof Explorer

Theorem ssequn1

Description: A relationship between subclass and union. Theorem 26 of Suppes p. 27. (Contributed by NM, 30-Aug-1993) (Proof shortened by Andrew Salmon, 26-Jun-2011)

Ref Expression
Assertion ssequn1 ⊢ A ⊆ B ↔ A ∪ B = B

Proof

Step Hyp Ref Expression
1 bicom ⊢ x ∈ B ↔ x ∈ A ∨ x ∈ B ↔ x ∈ A ∨ x ∈ B ↔ x ∈ B
2 pm4.72 ⊢ x ∈ A → x ∈ B ↔ x ∈ B ↔ x ∈ A ∨ x ∈ B
3 elun ⊢ x ∈ A ∪ B ↔ x ∈ A ∨ x ∈ B
4 3 bibi1i ⊢ x ∈ A ∪ B ↔ x ∈ B ↔ x ∈ A ∨ x ∈ B ↔ x ∈ B
5 1 2 4 3bitr4i ⊢ x ∈ A → x ∈ B ↔ x ∈ A ∪ B ↔ x ∈ B
6 5 albii ⊢ ∀ x x ∈ A → x ∈ B ↔ ∀ x x ∈ A ∪ B ↔ x ∈ B
7 df-ss ⊢ A ⊆ B ↔ ∀ x x ∈ A → x ∈ B
8 dfcleq ⊢ A ∪ B = B ↔ ∀ x x ∈ A ∪ B ↔ x ∈ B
9 6 7 8 3bitr4i ⊢ A ⊆ B ↔ A ∪ B = B