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 BAABCA=BA=BC

Proof

Step Hyp Ref Expression
1 ssunsn2 BAABCBAABBCAABC
2 ancom BAABABBA
3 eqss A=BABBA
4 2 3 bitr4i BAABA=B
5 ancom BCAABCABCBCA
6 eqss A=BCABCBCA
7 5 6 bitr4i BCAABCA=BC
8 4 7 orbi12i BAABBCAABCA=BA=BC
9 1 8 bitri BAABCA=BA=BC