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 = { 𝑥 ∣ ∃ 𝑦 𝑦 E 𝑥 }
2		nfab1	⊢ Ⅎ 𝑥 { 𝑥 ∣ ∃ 𝑦 𝑦 E 𝑥 }
3		nfcv	⊢ Ⅎ 𝑥 ( V ∖ { ∅ } )
4		abid	⊢ ( 𝑥 ∈ { 𝑥 ∣ ∃ 𝑦 𝑦 E 𝑥 } ↔ ∃ 𝑦 𝑦 E 𝑥 )
5		epel	⊢ ( 𝑦 E 𝑥 ↔ 𝑦 ∈ 𝑥 )
6	5	exbii	⊢ ( ∃ 𝑦 𝑦 E 𝑥 ↔ ∃ 𝑦 𝑦 ∈ 𝑥 )
7		neq0	⊢ ( ¬ 𝑥 = ∅ ↔ ∃ 𝑦 𝑦 ∈ 𝑥 )
8	7	bicomi	⊢ ( ∃ 𝑦 𝑦 ∈ 𝑥 ↔ ¬ 𝑥 = ∅ )
9		velsn	⊢ ( 𝑥 ∈ { ∅ } ↔ 𝑥 = ∅ )
10	9	bicomi	⊢ ( 𝑥 = ∅ ↔ 𝑥 ∈ { ∅ } )
11	10	notbii	⊢ ( ¬ 𝑥 = ∅ ↔ ¬ 𝑥 ∈ { ∅ } )
12	6 8 11	3bitri	⊢ ( ∃ 𝑦 𝑦 E 𝑥 ↔ ¬ 𝑥 ∈ { ∅ } )
13		velcomp	⊢ ( 𝑥 ∈ ( V ∖ { ∅ } ) ↔ ¬ 𝑥 ∈ { ∅ } )
14	13	bicomi	⊢ ( ¬ 𝑥 ∈ { ∅ } ↔ 𝑥 ∈ ( V ∖ { ∅ } ) )
15	4 12 14	3bitri	⊢ ( 𝑥 ∈ { 𝑥 ∣ ∃ 𝑦 𝑦 E 𝑥 } ↔ 𝑥 ∈ ( V ∖ { ∅ } ) )
16	2 3 15	eqri	⊢ { 𝑥 ∣ ∃ 𝑦 𝑦 E 𝑥 } = ( V ∖ { ∅ } )
17	1 16	eqtri	⊢ ran E = ( V ∖ { ∅ } )