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 ∖ { ∅ } )