Theorem dmcnvepres

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

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

Proof

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