Theorem ecunres

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

	Ref	Expression
Assertion	ecunres	⊢ ( 𝐵 ∈ 𝑉 → [ 𝐵 ] ( ( 𝑅 ∪ 𝑆 ) ↾ 𝐴 ) = ( [ 𝐵 ] ( 𝑅 ↾ 𝐴 ) ∪ [ 𝐵 ] ( 𝑆 ↾ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		resundir	⊢ ( ( 𝑅 ∪ 𝑆 ) ↾ 𝐴 ) = ( ( 𝑅 ↾ 𝐴 ) ∪ ( 𝑆 ↾ 𝐴 ) )
2	1	eceq2i	⊢ [ 𝐵 ] ( ( 𝑅 ∪ 𝑆 ) ↾ 𝐴 ) = [ 𝐵 ] ( ( 𝑅 ↾ 𝐴 ) ∪ ( 𝑆 ↾ 𝐴 ) )
3		ecun	⊢ ( 𝐵 ∈ 𝑉 → [ 𝐵 ] ( ( 𝑅 ↾ 𝐴 ) ∪ ( 𝑆 ↾ 𝐴 ) ) = ( [ 𝐵 ] ( 𝑅 ↾ 𝐴 ) ∪ [ 𝐵 ] ( 𝑆 ↾ 𝐴 ) ) )
4	2 3	eqtrid	⊢ ( 𝐵 ∈ 𝑉 → [ 𝐵 ] ( ( 𝑅 ∪ 𝑆 ) ↾ 𝐴 ) = ( [ 𝐵 ] ( 𝑅 ↾ 𝐴 ) ∪ [ 𝐵 ] ( 𝑆 ↾ 𝐴 ) ) )