This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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 } ) ) )