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 C_ A /\ A C_ ( B u. { C } ) ) <-> ( A = B \/ A = ( B u. { C } ) ) )

Proof

Step	Hyp	Ref	Expression
1		ssunsn2	|- ( ( B C_ A /\ A C_ ( B u. { C } ) ) <-> ( ( B C_ A /\ A C_ B ) \/ ( ( B u. { C } ) C_ A /\ A C_ ( B u. { C } ) ) ) )
2		ancom	|- ( ( B C_ A /\ A C_ B ) <-> ( A C_ B /\ B C_ A ) )
3		eqss	|- ( A = B <-> ( A C_ B /\ B C_ A ) )
4	2 3	bitr4i	|- ( ( B C_ A /\ A C_ B ) <-> A = B )
5		ancom	|- ( ( ( B u. { C } ) C_ A /\ A C_ ( B u. { C } ) ) <-> ( A C_ ( B u. { C } ) /\ ( B u. { C } ) C_ A ) )
6		eqss	|- ( A = ( B u. { C } ) <-> ( A C_ ( B u. { C } ) /\ ( B u. { C } ) C_ A ) )
7	5 6	bitr4i	|- ( ( ( B u. { C } ) C_ A /\ A C_ ( B u. { C } ) ) <-> A = ( B u. { C } ) )
8	4 7	orbi12i	|- ( ( ( B C_ A /\ A C_ B ) \/ ( ( B u. { C } ) C_ A /\ A C_ ( B u. { C } ) ) ) <-> ( A = B \/ A = ( B u. { C } ) ) )
9	1 8	bitri	|- ( ( B C_ A /\ A C_ ( B u. { C } ) ) <-> ( A = B \/ A = ( B u. { C } ) ) )