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 = { 𝑥 ∣ ∃ 𝑦 𝑦 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 ∖ { ∅ } )