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