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

Metamath Proof Explorer

Theorem sspr

Description: The subsets of a pair. (Contributed by NM, 16-Mar-2006) (Proof shortened by Mario Carneiro, 2-Jul-2016)

Ref Expression
Assertion sspr 
|- ( A C_ { B , C } <-> ( ( A = (/) \/ A = { B } ) \/ ( A = { C } \/ A = { B , C } ) ) )

Proof

Step Hyp Ref Expression
1 0un 
 |-  ( (/) u. { B , C } ) = { B , C }
2 1 sseq2i 
 |-  ( A C_ ( (/) u. { B , C } ) <-> A C_ { B , C } )
3 0ss 
 |-  (/) C_ A
4 3 biantrur 
 |-  ( A C_ ( (/) u. { B , C } ) <-> ( (/) C_ A /\ A C_ ( (/) u. { B , C } ) ) )
5 2 4 bitr3i 
 |-  ( A C_ { B , C } <-> ( (/) C_ A /\ A C_ ( (/) u. { B , C } ) ) )
6 ssunpr 
 |-  ( ( (/) C_ A /\ A C_ ( (/) u. { B , C } ) ) <-> ( ( A = (/) \/ A = ( (/) u. { B } ) ) \/ ( A = ( (/) u. { C } ) \/ A = ( (/) u. { B , C } ) ) ) )
7 0un 
 |-  ( (/) u. { B } ) = { B }
8 7 eqeq2i 
 |-  ( A = ( (/) u. { B } ) <-> A = { B } )
9 8 orbi2i 
 |-  ( ( A = (/) \/ A = ( (/) u. { B } ) ) <-> ( A = (/) \/ A = { B } ) )
10 0un 
 |-  ( (/) u. { C } ) = { C }
11 10 eqeq2i 
 |-  ( A = ( (/) u. { C } ) <-> A = { C } )
12 1 eqeq2i 
 |-  ( A = ( (/) u. { B , C } ) <-> A = { B , C } )
13 11 12 orbi12i 
 |-  ( ( A = ( (/) u. { C } ) \/ A = ( (/) u. { B , C } ) ) <-> ( A = { C } \/ A = { B , C } ) )
14 9 13 orbi12i 
 |-  ( ( ( A = (/) \/ A = ( (/) u. { B } ) ) \/ ( A = ( (/) u. { C } ) \/ A = ( (/) u. { B , C } ) ) ) <-> ( ( A = (/) \/ A = { B } ) \/ ( A = { C } \/ A = { B , C } ) ) )
15 5 6 14 3bitri 
 |-  ( A C_ { B , C } <-> ( ( A = (/) \/ A = { B } ) \/ ( A = { C } \/ A = { B , C } ) ) )