Theorem dmcnvep

Description: Domain of converse epsilon relation. (Contributed by Peter Mazsa, 30-Jan-2018) (Revised by Peter Mazsa, 23-Nov-2025)

	Ref	Expression
Assertion	dmcnvep	$$⊢\mathrm{dom}{\mathrm{E}}^{-1}=\mathrm{V}\setminus \left\{\varnothing \right\}$$

Proof

Step	Hyp	Ref	Expression
1		df-dm	$$⊢\mathrm{dom}{\mathrm{E}}^{-1}=\left\{x|\exists yx{\mathrm{E}}^{-1}y\right\}$$
2		brcnvep	$$⊢x\in \mathrm{V}\to \left(x{\mathrm{E}}^{-1}y\leftrightarrow y\in x\right)$$
3	2	elv	$$⊢x{\mathrm{E}}^{-1}y\leftrightarrow y\in x$$
4	3	exbii	$$⊢\exists yx{\mathrm{E}}^{-1}y\leftrightarrow \exists yy\in x$$
5	4	abbii	$$⊢\left\{x|\exists yx{\mathrm{E}}^{-1}y\right\}=\left\{x|\exists yy\in x\right\}$$
6		df-sn	$$⊢\left\{\varnothing \right\}=\left\{x|x=\varnothing \right\}$$
7	6	difeq2i	$$⊢\mathrm{V}\setminus \left\{\varnothing \right\}=\mathrm{V}\setminus \left\{x|x=\varnothing \right\}$$
8		notab	$$⊢\left\{x|\neg x=\varnothing \right\}=\mathrm{V}\setminus \left\{x|x=\varnothing \right\}$$
9		neq0	$$⊢\neg x=\varnothing \leftrightarrow \exists yy\in x$$
10	9	abbii	$$⊢\left\{x|\neg x=\varnothing \right\}=\left\{x|\exists yy\in x\right\}$$
11	7 8 10	3eqtr2ri	$$⊢\left\{x|\exists yy\in x\right\}=\mathrm{V}\setminus \left\{\varnothing \right\}$$
12	1 5 11	3eqtri	$$⊢\mathrm{dom}{\mathrm{E}}^{-1}=\mathrm{V}\setminus \left\{\varnothing \right\}$$