Theorem ssunpr

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

Proof

Step	Hyp	Ref	Expression
1		df-pr	|- { C , D } = ( { C } u. { D } )
2	1	uneq2i	|- ( B u. { C , D } ) = ( B u. ( { C } u. { D } ) )
3		unass	|- ( ( B u. { C } ) u. { D } ) = ( B u. ( { C } u. { D } ) )
4	2 3	eqtr4i	|- ( B u. { C , D } ) = ( ( B u. { C } ) u. { D } )
5	4	sseq2i	|- ( A C_ ( B u. { C , D } ) <-> A C_ ( ( B u. { C } ) u. { D } ) )
6	5	anbi2i	|- ( ( B C_ A /\ A C_ ( B u. { C , D } ) ) <-> ( B C_ A /\ A C_ ( ( B u. { C } ) u. { D } ) ) )
7		ssunsn2	|- ( ( B C_ A /\ A C_ ( ( B u. { C } ) u. { D } ) ) <-> ( ( B C_ A /\ A C_ ( B u. { C } ) ) \/ ( ( B u. { D } ) C_ A /\ A C_ ( ( B u. { C } ) u. { D } ) ) ) )
8		ssunsn	|- ( ( B C_ A /\ A C_ ( B u. { C } ) ) <-> ( A = B \/ A = ( B u. { C } ) ) )
9		un23	|- ( ( B u. { C } ) u. { D } ) = ( ( B u. { D } ) u. { C } )
10	9	sseq2i	|- ( A C_ ( ( B u. { C } ) u. { D } ) <-> A C_ ( ( B u. { D } ) u. { C } ) )
11	10	anbi2i	|- ( ( ( B u. { D } ) C_ A /\ A C_ ( ( B u. { C } ) u. { D } ) ) <-> ( ( B u. { D } ) C_ A /\ A C_ ( ( B u. { D } ) u. { C } ) ) )
12		ssunsn	|- ( ( ( B u. { D } ) C_ A /\ A C_ ( ( B u. { D } ) u. { C } ) ) <-> ( A = ( B u. { D } ) \/ A = ( ( B u. { D } ) u. { C } ) ) )
13	4 9	eqtr2i	|- ( ( B u. { D } ) u. { C } ) = ( B u. { C , D } )
14	13	eqeq2i	|- ( A = ( ( B u. { D } ) u. { C } ) <-> A = ( B u. { C , D } ) )
15	14	orbi2i	|- ( ( A = ( B u. { D } ) \/ A = ( ( B u. { D } ) u. { C } ) ) <-> ( A = ( B u. { D } ) \/ A = ( B u. { C , D } ) ) )
16	11 12 15	3bitri	|- ( ( ( B u. { D } ) C_ A /\ A C_ ( ( B u. { C } ) u. { D } ) ) <-> ( A = ( B u. { D } ) \/ A = ( B u. { C , D } ) ) )
17	8 16	orbi12i	|- ( ( ( B C_ A /\ A C_ ( B u. { C } ) ) \/ ( ( B u. { D } ) C_ A /\ A C_ ( ( B u. { C } ) u. { D } ) ) ) <-> ( ( A = B \/ A = ( B u. { C } ) ) \/ ( A = ( B u. { D } ) \/ A = ( B u. { C , D } ) ) ) )
18	6 7 17	3bitri	|- ( ( B C_ A /\ A C_ ( B u. { C , D } ) ) <-> ( ( A = B \/ A = ( B u. { C } ) ) \/ ( A = ( B u. { D } ) \/ A = ( B u. { C , D } ) ) ) )