This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dmuncnvepres

Description: Domain of the union with the converse epsilon, restricted. (Contributed by Peter Mazsa, 28-Jan-2026)

Ref Expression
Assertion dmuncnvepres ⊢ dom ⁡ R ∪ E -1 ↾ A = A ∩ dom ⁡ R ∪ V ∖ ∅

Proof

Step Hyp Ref Expression
1 dmres ⊢ dom ⁡ R ∪ E -1 ↾ A = A ∩ dom ⁡ R ∪ E -1
2 dmun ⊢ dom ⁡ R ∪ E -1 = dom ⁡ R ∪ dom ⁡ E -1
3 dmcnvep ⊢ dom ⁡ E -1 = V ∖ ∅
4 3 uneq2i ⊢ dom ⁡ R ∪ dom ⁡ E -1 = dom ⁡ R ∪ V ∖ ∅
5 2 4 eqtri ⊢ dom ⁡ R ∪ E -1 = dom ⁡ R ∪ V ∖ ∅
6 5 ineq2i ⊢ A ∩ dom ⁡ R ∪ E -1 = A ∩ dom ⁡ R ∪ V ∖ ∅
7 1 6 eqtri ⊢ dom ⁡ R ∪ E -1 ↾ A = A ∩ dom ⁡ R ∪ V ∖ ∅