Metamath Proof Explorer

Theorem bj-unrab

Description: Generalization of unrab . Equality need not hold. (Contributed by BJ, 21-Apr-2019)

Ref Expression
Assertion bj-unrab 
|- ( { x e. A | ph } u. { x e. B | ps } ) C_ { x e. ( A u. B ) | ( ph \/ ps ) }

Proof

Step Hyp Ref Expression
1 ssun1 
 |-  A C_ ( A u. B )
2 rabss2 
 |-  ( A C_ ( A u. B ) -> { x e. A | ph } C_ { x e. ( A u. B ) | ph } )
3 1 2 ax-mp 
 |-  { x e. A | ph } C_ { x e. ( A u. B ) | ph }
4 orc 
 |-  ( ph -> ( ph \/ ps ) )
5 4 a1i 
 |-  ( x e. ( A u. B ) -> ( ph -> ( ph \/ ps ) ) )
6 5 ss2rabi 
 |-  { x e. ( A u. B ) | ph } C_ { x e. ( A u. B ) | ( ph \/ ps ) }
7 3 6 sstri 
 |-  { x e. A | ph } C_ { x e. ( A u. B ) | ( ph \/ ps ) }
8 ssun2 
 |-  B C_ ( A u. B )
9 rabss2 
 |-  ( B C_ ( A u. B ) -> { x e. B | ps } C_ { x e. ( A u. B ) | ps } )
10 8 9 ax-mp 
 |-  { x e. B | ps } C_ { x e. ( A u. B ) | ps }
11 olc 
 |-  ( ps -> ( ph \/ ps ) )
12 11 a1i 
 |-  ( x e. ( A u. B ) -> ( ps -> ( ph \/ ps ) ) )
13 12 ss2rabi 
 |-  { x e. ( A u. B ) | ps } C_ { x e. ( A u. B ) | ( ph \/ ps ) }
14 10 13 sstri 
 |-  { x e. B | ps } C_ { x e. ( A u. B ) | ( ph \/ ps ) }
15 7 14 unssi 
 |-  ( { x e. A | ph } u. { x e. B | ps } ) C_ { x e. ( A u. B ) | ( ph \/ ps ) }