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

Metamath Proof Explorer

Theorem dmxrncnvepres2

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

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

Proof

Step Hyp Ref Expression
1 dmres ⊢ dom ⁡ R ↾ A = A ∩ dom ⁡ R
2 1 difeq1i ⊢ dom ⁡ R ↾ A ∖ ∅ = A ∩ dom ⁡ R ∖ ∅
3 dmxrncnvepres ⊢ dom ⁡ R ⋉ E -1 ↾ A = dom ⁡ R ↾ A ∖ ∅
4 indif2 ⊢ A ∩ dom ⁡ R ∖ ∅ = A ∩ dom ⁡ R ∖ ∅
5 2 3 4 3eqtr4i ⊢ dom ⁡ R ⋉ E -1 ↾ A = A ∩ dom ⁡ R ∖ ∅