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 uncom 
 |-  ( (/) u. { B , C } ) = ( { B , C } u. (/) )
2 un0 
 |-  ( { B , C } u. (/) ) = { B , C }
3 1 2 eqtri 
 |-  ( (/) u. { B , C } ) = { B , C }
4 3 sseq2i 
 |-  ( A C_ ( (/) u. { B , C } ) <-> A C_ { B , C } )
5 0ss 
 |-  (/) C_ A
6 5 biantrur 
 |-  ( A C_ ( (/) u. { B , C } ) <-> ( (/) C_ A /\ A C_ ( (/) u. { B , C } ) ) )
7 4 6 bitr3i 
 |-  ( A C_ { B , C } <-> ( (/) C_ A /\ A C_ ( (/) u. { B , C } ) ) )
8 ssunpr 
 |-  ( ( (/) C_ A /\ A C_ ( (/) u. { B , C } ) ) <-> ( ( A = (/) \/ A = ( (/) u. { B } ) ) \/ ( A = ( (/) u. { C } ) \/ A = ( (/) u. { B , C } ) ) ) )
9 uncom 
 |-  ( (/) u. { B } ) = ( { B } u. (/) )
10 un0 
 |-  ( { B } u. (/) ) = { B }
11 9 10 eqtri 
 |-  ( (/) u. { B } ) = { B }
12 11 eqeq2i 
 |-  ( A = ( (/) u. { B } ) <-> A = { B } )
13 12 orbi2i 
 |-  ( ( A = (/) \/ A = ( (/) u. { B } ) ) <-> ( A = (/) \/ A = { B } ) )
14 uncom 
 |-  ( (/) u. { C } ) = ( { C } u. (/) )
15 un0 
 |-  ( { C } u. (/) ) = { C }
16 14 15 eqtri 
 |-  ( (/) u. { C } ) = { C }
17 16 eqeq2i 
 |-  ( A = ( (/) u. { C } ) <-> A = { C } )
18 3 eqeq2i 
 |-  ( A = ( (/) u. { B , C } ) <-> A = { B , C } )
19 17 18 orbi12i 
 |-  ( ( A = ( (/) u. { C } ) \/ A = ( (/) u. { B , C } ) ) <-> ( A = { C } \/ A = { B , C } ) )
20 13 19 orbi12i 
 |-  ( ( ( A = (/) \/ A = ( (/) u. { B } ) ) \/ ( A = ( (/) u. { C } ) \/ A = ( (/) u. { B , C } ) ) ) <-> ( ( A = (/) \/ A = { B } ) \/ ( A = { C } \/ A = { B , C } ) ) )
21 7 8 20 3bitri 
 |-  ( A C_ { B , C } <-> ( ( A = (/) \/ A = { B } ) \/ ( A = { C } \/ A = { B , C } ) ) )