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