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

Metamath Proof Explorer

Theorem dmcnvep

Description: Domain of converse epsilon relation. (Contributed by Peter Mazsa, 30-Jan-2018) (Revised by Peter Mazsa, 23-Nov-2025)

Ref Expression
Assertion dmcnvep dom ◡ E = ( V ∖ { ∅ } )

Proof

Step Hyp Ref Expression
1 df-dm ⊢ dom ◡ E = { 𝑥 ∣ ∃ 𝑦 𝑥 ◡ E 𝑦 }
2 brcnvep ⊢ ( 𝑥 ∈ V → ( 𝑥 ◡ E 𝑦 ↔ 𝑦 ∈ 𝑥 ) )
3 2 elv ⊢ ( 𝑥 ◡ E 𝑦 ↔ 𝑦 ∈ 𝑥 )
4 3 exbii ⊢ ( ∃ 𝑦 𝑥 ◡ E 𝑦 ↔ ∃ 𝑦 𝑦 ∈ 𝑥 )
5 4 abbii ⊢ { 𝑥 ∣ ∃ 𝑦 𝑥 ◡ E 𝑦 } = { 𝑥 ∣ ∃ 𝑦 𝑦 ∈ 𝑥 }
6 df-sn ⊢ { ∅ } = { 𝑥 ∣ 𝑥 = ∅ }
7 6 difeq2i ⊢ ( V ∖ { ∅ } ) = ( V ∖ { 𝑥 ∣ 𝑥 = ∅ } )
8 notab ⊢ { 𝑥 ∣ ¬ 𝑥 = ∅ } = ( V ∖ { 𝑥 ∣ 𝑥 = ∅ } )
9 neq0 ⊢ ( ¬ 𝑥 = ∅ ↔ ∃ 𝑦 𝑦 ∈ 𝑥 )
10 9 abbii ⊢ { 𝑥 ∣ ¬ 𝑥 = ∅ } = { 𝑥 ∣ ∃ 𝑦 𝑦 ∈ 𝑥 }
11 7 8 10 3eqtr2ri ⊢ { 𝑥 ∣ ∃ 𝑦 𝑦 ∈ 𝑥 } = ( V ∖ { ∅ } )
12 1 5 11 3eqtri ⊢ dom ◡ E = ( V ∖ { ∅ } )