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

Metamath Proof Explorer

Theorem 3unrab

Description: Union of three restricted class abstractions. (Contributed by Thierry Arnoux, 6-Jul-2025)

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

Proof

Step Hyp Ref Expression
1 unrab 
 |-  ( { x e. A | ( ph \/ ps ) } u. { x e. A | ch } ) = { x e. A | ( ( ph \/ ps ) \/ ch ) }
2 unrab 
 |-  ( { x e. A | ph } u. { x e. A | ps } ) = { x e. A | ( ph \/ ps ) }
3 2 uneq1i 
 |-  ( ( { x e. A | ph } u. { x e. A | ps } ) u. { x e. A | ch } ) = ( { x e. A | ( ph \/ ps ) } u. { x e. A | ch } )
4 df-3or 
 |-  ( ( ph \/ ps \/ ch ) <-> ( ( ph \/ ps ) \/ ch ) )
5 4 rabbii 
 |-  { x e. A | ( ph \/ ps \/ ch ) } = { x e. A | ( ( ph \/ ps ) \/ ch ) }
6 1 3 5 3eqtr4i 
 |-  ( ( { x e. A | ph } u. { x e. A | ps } ) u. { x e. A | ch } ) = { x e. A | ( ph \/ ps \/ ch ) }