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