Theorem ecunres

Description: The restricted union coset of B . (Contributed by Peter Mazsa, 28-Jan-2026)

	Ref	Expression
Assertion	ecunres	|- ( B e. V -> [ B ] ( ( R u. S ) |` A ) = ( [ B ] ( R |` A ) u. [ B ] ( S |` A ) ) )

Proof

Step	Hyp	Ref	Expression
1		resundir	|- ( ( R u. S ) |` A ) = ( ( R |` A ) u. ( S |` A ) )
2	1	eceq2i	|- [ B ] ( ( R u. S ) |` A ) = [ B ] ( ( R |` A ) u. ( S |` A ) )
3		ecun	|- ( B e. V -> [ B ] ( ( R |` A ) u. ( S |` A ) ) = ( [ B ] ( R |` A ) u. [ B ] ( S |` A ) ) )
4	2 3	eqtrid	|- ( B e. V -> [ B ] ( ( R u. S ) |` A ) = ( [ B ] ( R |` A ) u. [ B ] ( S |` A ) ) )