Theorem dmxrncnvep

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

	Ref	Expression
Assertion	dmxrncnvep	$$⊢\mathrm{dom}R⋉{\mathrm{E}}^{-1}=\mathrm{dom}R\setminus \left\{\varnothing \right\}$$

Proof

Step	Hyp	Ref	Expression
1		dmxrn	$$⊢\mathrm{dom}R⋉{\mathrm{E}}^{-1}=\mathrm{dom}R\cap \mathrm{dom}{\mathrm{E}}^{-1}$$
2		dmcnvep	$$⊢\mathrm{dom}{\mathrm{E}}^{-1}=\mathrm{V}\setminus \left\{\varnothing \right\}$$
3	2	ineq2i	$$⊢\mathrm{dom}R\cap \mathrm{dom}{\mathrm{E}}^{-1}=\mathrm{dom}R\cap \left(\mathrm{V}\setminus \left\{\varnothing \right\}\right)$$
4		invdif	$$⊢\mathrm{dom}R\cap \left(\mathrm{V}\setminus \left\{\varnothing \right\}\right)=\mathrm{dom}R\setminus \left\{\varnothing \right\}$$
5	1 3 4	3eqtri	$$⊢\mathrm{dom}R⋉{\mathrm{E}}^{-1}=\mathrm{dom}R\setminus \left\{\varnothing \right\}$$