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

Metamath Proof Explorer

Theorem dmxrncnvepres

Description: Domain of the range product with restricted converse epsilon relation. (Contributed by Peter Mazsa, 23-Nov-2025)

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

Proof

Step Hyp Ref Expression
1 xrnres ⊢ R ⋉ E -1 ↾ A = R ↾ A ⋉ E -1
2 xrnres2 ⊢ R ⋉ E -1 ↾ A = R ⋉ E -1 ↾ A
3 1 2 eqtr3i ⊢ R ↾ A ⋉ E -1 = R ⋉ E -1 ↾ A
4 3 dmeqi ⊢ dom ⁡ R ↾ A ⋉ E -1 = dom ⁡ R ⋉ E -1 ↾ A
5 dmxrncnvep ⊢ dom ⁡ R ↾ A ⋉ E -1 = dom ⁡ R ↾ A ∖ ∅
6 4 5 eqtr3i ⊢ dom ⁡ R ⋉ E -1 ↾ A = dom ⁡ R ↾ A ∖ ∅