Theorem rnep

Description: The range of the membership relation is the universal class minus the empty set. (Contributed by BJ, 26-Dec-2023)

	Ref	Expression
Assertion	rnep	$$⊢\mathrm{ran}\mathrm{E}=\mathrm{V}\setminus \left\{\varnothing \right\}$$

Proof

Step	Hyp	Ref	Expression
1		dfrn2	$$⊢\mathrm{ran}\mathrm{E}=\left\{x|\exists yy\mathrm{E}x\right\}$$
2		nfab1	$$⊢\underset{\_}{Ⅎ}x\left\{x|\exists yy\mathrm{E}x\right\}$$
3		nfcv	$$⊢\underset{\_}{Ⅎ}x\left(\mathrm{V}\setminus \left\{\varnothing \right\}\right)$$
4		abid	$$⊢x\in \left\{x|\exists yy\mathrm{E}x\right\}\leftrightarrow \exists yy\mathrm{E}x$$
5		epel	$$⊢y\mathrm{E}x\leftrightarrow y\in x$$
6	5	exbii	$$⊢\exists yy\mathrm{E}x\leftrightarrow \exists yy\in x$$
7		neq0	$$⊢\neg x=\varnothing \leftrightarrow \exists yy\in x$$
8	7	bicomi	$$⊢\exists yy\in x\leftrightarrow \neg x=\varnothing$$
9		velsn	$$⊢x\in \left\{\varnothing \right\}\leftrightarrow x=\varnothing$$
10	9	bicomi	$$⊢x=\varnothing \leftrightarrow x\in \left\{\varnothing \right\}$$
11	10	notbii	$$⊢\neg x=\varnothing \leftrightarrow \neg x\in \left\{\varnothing \right\}$$
12	6 8 11	3bitri	$$⊢\exists yy\mathrm{E}x\leftrightarrow \neg x\in \left\{\varnothing \right\}$$
13		velcomp	$$⊢x\in \left(\mathrm{V}\setminus \left\{\varnothing \right\}\right)\leftrightarrow \neg x\in \left\{\varnothing \right\}$$
14	13	bicomi	$$⊢\neg x\in \left\{\varnothing \right\}\leftrightarrow x\in \left(\mathrm{V}\setminus \left\{\varnothing \right\}\right)$$
15	4 12 14	3bitri	$$⊢x\in \left\{x|\exists yy\mathrm{E}x\right\}\leftrightarrow x\in \left(\mathrm{V}\setminus \left\{\varnothing \right\}\right)$$
16	2 3 15	eqri	$$⊢\left\{x|\exists yy\mathrm{E}x\right\}=\mathrm{V}\setminus \left\{\varnothing \right\}$$
17	1 16	eqtri	$$⊢\mathrm{ran}\mathrm{E}=\mathrm{V}\setminus \left\{\varnothing \right\}$$