Metamath Proof Explorer

Theorem unrab

Description: Union of two restricted class abstractions. (Contributed by NM, 25-Mar-2004)

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

Proof

Step Hyp Ref Expression
1 df-rab 
 |-  { x e. A | ph } = { x | ( x e. A /\ ph ) }
2 df-rab 
 |-  { x e. A | ps } = { x | ( x e. A /\ ps ) }
3 1 2 uneq12i 
 |-  ( { x e. A | ph } u. { x e. A | ps } ) = ( { x | ( x e. A /\ ph ) } u. { x | ( x e. A /\ ps ) } )
4 df-rab 
 |-  { x e. A | ( ph \/ ps ) } = { x | ( x e. A /\ ( ph \/ ps ) ) }
5 unab 
 |-  ( { x | ( x e. A /\ ph ) } u. { x | ( x e. A /\ ps ) } ) = { x | ( ( x e. A /\ ph ) \/ ( x e. A /\ ps ) ) }
6 andi 
 |-  ( ( x e. A /\ ( ph \/ ps ) ) <-> ( ( x e. A /\ ph ) \/ ( x e. A /\ ps ) ) )
7 6 abbii 
 |-  { x | ( x e. A /\ ( ph \/ ps ) ) } = { x | ( ( x e. A /\ ph ) \/ ( x e. A /\ ps ) ) }
8 5 7 eqtr4i 
 |-  ( { x | ( x e. A /\ ph ) } u. { x | ( x e. A /\ ps ) } ) = { x | ( x e. A /\ ( ph \/ ps ) ) }
9 4 8 eqtr4i 
 |-  { x e. A | ( ph \/ ps ) } = ( { x | ( x e. A /\ ph ) } u. { x | ( x e. A /\ ps ) } )
10 3 9 eqtr4i 
 |-  ( { x e. A | ph } u. { x e. A | ps } ) = { x e. A | ( ph \/ ps ) }