Metamath Proof Explorer

Theorem ssunsn

Description: Possible values for a set sandwiched between another set and it plus a singleton. (Contributed by Mario Carneiro, 2-Jul-2016)

Ref Expression
Assertion ssunsn ⊢ B ⊆ A ∧ A ⊆ B ∪ C ↔ A = B ∨ A = B ∪ C

Proof

Step Hyp Ref Expression
1 ssunsn2 ⊢ B ⊆ A ∧ A ⊆ B ∪ C ↔ B ⊆ A ∧ A ⊆ B ∨ B ∪ C ⊆ A ∧ A ⊆ B ∪ C
2 ancom ⊢ B ⊆ A ∧ A ⊆ B ↔ A ⊆ B ∧ B ⊆ A
3 eqss ⊢ A = B ↔ A ⊆ B ∧ B ⊆ A
4 2 3 bitr4i ⊢ B ⊆ A ∧ A ⊆ B ↔ A = B
5 ancom ⊢ B ∪ C ⊆ A ∧ A ⊆ B ∪ C ↔ A ⊆ B ∪ C ∧ B ∪ C ⊆ A
6 eqss ⊢ A = B ∪ C ↔ A ⊆ B ∪ C ∧ B ∪ C ⊆ A
7 5 6 bitr4i ⊢ B ∪ C ⊆ A ∧ A ⊆ B ∪ C ↔ A = B ∪ C
8 4 7 orbi12i ⊢ B ⊆ A ∧ A ⊆ B ∨ B ∪ C ⊆ A ∧ A ⊆ B ∪ C ↔ A = B ∨ A = B ∪ C
9 1 8 bitri ⊢ B ⊆ A ∧ A ⊆ B ∪ C ↔ A = B ∨ A = B ∪ C