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

Metamath Proof Explorer

Theorem dmxrnuncnvepres

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

Ref Expression
Assertion dmxrnuncnvepres ⊢ dom ⁡ R ⋉ E -1 ∪ E -1 ↾ A = A ∖ ∅

Proof

Step Hyp Ref Expression
1 dmuncnvepres ⊢ dom ⁡ R ⋉ E -1 ∪ E -1 ↾ A = A ∩ dom ⁡ R ⋉ E -1 ∪ V ∖ ∅
2 dmxrncnvep ⊢ dom ⁡ R ⋉ E -1 = dom ⁡ R ∖ ∅
3 2 uneq1i ⊢ dom ⁡ R ⋉ E -1 ∪ V ∖ ∅ = dom ⁡ R ∖ ∅ ∪ V ∖ ∅
4 difundir ⊢ dom ⁡ R ∪ V ∖ ∅ = dom ⁡ R ∖ ∅ ∪ V ∖ ∅
5 unv ⊢ dom ⁡ R ∪ V = V
6 5 difeq1i ⊢ dom ⁡ R ∪ V ∖ ∅ = V ∖ ∅
7 3 4 6 3eqtr2i ⊢ dom ⁡ R ⋉ E -1 ∪ V ∖ ∅ = V ∖ ∅
8 7 ineq2i ⊢ A ∩ dom ⁡ R ⋉ E -1 ∪ V ∖ ∅ = A ∩ V ∖ ∅
9 invdif ⊢ A ∩ V ∖ ∅ = A ∖ ∅
10 1 8 9 3eqtri ⊢ dom ⁡ R ⋉ E -1 ∪ E -1 ↾ A = A ∖ ∅