Metamath Proof Explorer

Theorem ecuncnvepres

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

Ref Expression
Assertion ecuncnvepres ⊢ B ∈ A → B R ∪ E -1 ↾ A = B ∪ B R

Proof

Step Hyp Ref Expression
1 ecunres ⊢ B ∈ A → B R ∪ E -1 ↾ A = B R ↾ A ∪ B E -1 ↾ A
2 elecreseq ⊢ B ∈ A → B R ↾ A = B R
3 eccnvepres2 ⊢ B ∈ A → B E -1 ↾ A = B
4 2 3 uneq12d ⊢ B ∈ A → B R ↾ A ∪ B E -1 ↾ A = B R ∪ B
5 1 4 eqtrd ⊢ B ∈ A → B R ∪ E -1 ↾ A = B R ∪ B
6 uncom ⊢ B R ∪ B = B ∪ B R
7 5 6 eqtrdi ⊢ B ∈ A → B R ∪ E -1 ↾ A = B ∪ B R