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 ) }