# Metamath Proof Explorer

## 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 {y}\phantom{\rule{.4em}{0ex}}{y}\mathrm{E}{x}\right\}$
2 nfab1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left\{{x}|\exists {y}\phantom{\rule{.4em}{0ex}}{y}\mathrm{E}{x}\right\}$
3 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left(\mathrm{V}\setminus \left\{\varnothing \right\}\right)$
4 abid ${⊢}{x}\in \left\{{x}|\exists {y}\phantom{\rule{.4em}{0ex}}{y}\mathrm{E}{x}\right\}↔\exists {y}\phantom{\rule{.4em}{0ex}}{y}\mathrm{E}{x}$
5 epel ${⊢}{y}\mathrm{E}{x}↔{y}\in {x}$
6 5 exbii ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}{y}\mathrm{E}{x}↔\exists {y}\phantom{\rule{.4em}{0ex}}{y}\in {x}$
7 neq0 ${⊢}¬{x}=\varnothing ↔\exists {y}\phantom{\rule{.4em}{0ex}}{y}\in {x}$
8 7 bicomi ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}{y}\in {x}↔¬{x}=\varnothing$
9 velsn ${⊢}{x}\in \left\{\varnothing \right\}↔{x}=\varnothing$
10 9 bicomi ${⊢}{x}=\varnothing ↔{x}\in \left\{\varnothing \right\}$
11 10 notbii ${⊢}¬{x}=\varnothing ↔¬{x}\in \left\{\varnothing \right\}$
12 6 8 11 3bitri ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}{y}\mathrm{E}{x}↔¬{x}\in \left\{\varnothing \right\}$
13 velcomp ${⊢}{x}\in \left(\mathrm{V}\setminus \left\{\varnothing \right\}\right)↔¬{x}\in \left\{\varnothing \right\}$
14 13 bicomi ${⊢}¬{x}\in \left\{\varnothing \right\}↔{x}\in \left(\mathrm{V}\setminus \left\{\varnothing \right\}\right)$
15 4 12 14 3bitri ${⊢}{x}\in \left\{{x}|\exists {y}\phantom{\rule{.4em}{0ex}}{y}\mathrm{E}{x}\right\}↔{x}\in \left(\mathrm{V}\setminus \left\{\varnothing \right\}\right)$
16 2 3 15 eqri ${⊢}\left\{{x}|\exists {y}\phantom{\rule{.4em}{0ex}}{y}\mathrm{E}{x}\right\}=\mathrm{V}\setminus \left\{\varnothing \right\}$
17 1 16 eqtri ${⊢}\mathrm{ran}\mathrm{E}=\mathrm{V}\setminus \left\{\varnothing \right\}$