# 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
`|- ran _E = ( _V \ { (/) } )`

### Proof

Step Hyp Ref Expression
1 dfrn2
` |-  ran _E = { x | E. y y _E x }`
2 nfab1
` |-  F/_ x { x | E. y y _E x }`
3 nfcv
` |-  F/_ x ( _V \ { (/) } )`
4 abid
` |-  ( x e. { x | E. y y _E x } <-> E. y y _E x )`
5 epel
` |-  ( y _E x <-> y e. x )`
6 5 exbii
` |-  ( E. y y _E x <-> E. y y e. x )`
7 neq0
` |-  ( -. x = (/) <-> E. y y e. x )`
8 7 bicomi
` |-  ( E. y y e. x <-> -. x = (/) )`
9 velsn
` |-  ( x e. { (/) } <-> x = (/) )`
10 9 bicomi
` |-  ( x = (/) <-> x e. { (/) } )`
11 10 notbii
` |-  ( -. x = (/) <-> -. x e. { (/) } )`
12 6 8 11 3bitri
` |-  ( E. y y _E x <-> -. x e. { (/) } )`
13 velcomp
` |-  ( x e. ( _V \ { (/) } ) <-> -. x e. { (/) } )`
14 13 bicomi
` |-  ( -. x e. { (/) } <-> x e. ( _V \ { (/) } ) )`
15 4 12 14 3bitri
` |-  ( x e. { x | E. y y _E x } <-> x e. ( _V \ { (/) } ) )`
16 2 3 15 eqri
` |-  { x | E. y y _E x } = ( _V \ { (/) } )`
17 1 16 eqtri
` |-  ran _E = ( _V \ { (/) } )`