Theorem dmuncnvepres

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

	Ref	Expression
Assertion	dmuncnvepres	$$⊢\mathrm{dom}\left({\left(R\cup {\mathrm{E}}^{-1}\right)\upharpoonright }_A\right)=A\cap \left(\mathrm{dom}R\cup \left(\mathrm{V}\setminus \left\{\varnothing \right\}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		dmres	$$⊢\mathrm{dom}\left({\left(R\cup {\mathrm{E}}^{-1}\right)\upharpoonright }_A\right)=A\cap \mathrm{dom}\left(R\cup {\mathrm{E}}^{-1}\right)$$
2		dmun	$$⊢\mathrm{dom}\left(R\cup {\mathrm{E}}^{-1}\right)=\mathrm{dom}R\cup \mathrm{dom}{\mathrm{E}}^{-1}$$
3		dmcnvep	$$⊢\mathrm{dom}{\mathrm{E}}^{-1}=\mathrm{V}\setminus \left\{\varnothing \right\}$$
4	3	uneq2i	$$⊢\mathrm{dom}R\cup \mathrm{dom}{\mathrm{E}}^{-1}=\mathrm{dom}R\cup \left(\mathrm{V}\setminus \left\{\varnothing \right\}\right)$$
5	2 4	eqtri	$$⊢\mathrm{dom}\left(R\cup {\mathrm{E}}^{-1}\right)=\mathrm{dom}R\cup \left(\mathrm{V}\setminus \left\{\varnothing \right\}\right)$$
6	5	ineq2i	$$⊢A\cap \mathrm{dom}\left(R\cup {\mathrm{E}}^{-1}\right)=A\cap \left(\mathrm{dom}R\cup \left(\mathrm{V}\setminus \left\{\varnothing \right\}\right)\right)$$
7	1 6	eqtri	$$⊢\mathrm{dom}\left({\left(R\cup {\mathrm{E}}^{-1}\right)\upharpoonright }_A\right)=A\cap \left(\mathrm{dom}R\cup \left(\mathrm{V}\setminus \left\{\varnothing \right\}\right)\right)$$