This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \ { (/) } )