Metamath Proof Explorer

Theorem ecunres

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

Ref Expression
Assertion ecunres ⊢ B ∈ V → B R ∪ S ↾ A = B R ↾ A ∪ B S ↾ A

Proof

Step Hyp Ref Expression
1 resundir ⊢ R ∪ S ↾ A = R ↾ A ∪ S ↾ A
2 1 eceq2i ⊢ B R ∪ S ↾ A = B R ↾ A ∪ S ↾ A
3 ecun ⊢ B ∈ V → B R ↾ A ∪ S ↾ A = B R ↾ A ∪ B S ↾ A
4 2 3 eqtrid ⊢ B ∈ V → B R ∪ S ↾ A = B R ↾ A ∪ B S ↾ A