Theorem dmcnvepres

Description: Domain of the restricted converse epsilon relation. (Contributed by Peter Mazsa, 28-Jan-2026)

	Ref	Expression
Assertion	dmcnvepres	⊢ dom ( ◡ E ↾ 𝐴 ) = ( 𝐴 ∖ { ∅ } )

Proof

Step	Hyp	Ref	Expression
1		dmres	⊢ dom ( ◡ E ↾ 𝐴 ) = ( 𝐴 ∩ dom ◡ E )
2		dmcnvep	⊢ dom ◡ E = ( V ∖ { ∅ } )
3	2	ineq2i	⊢ ( 𝐴 ∩ dom ◡ E ) = ( 𝐴 ∩ ( V ∖ { ∅ } ) )
4		invdif	⊢ ( 𝐴 ∩ ( V ∖ { ∅ } ) ) = ( 𝐴 ∖ { ∅ } )
5	1 3 4	3eqtri	⊢ dom ( ◡ E ↾ 𝐴 ) = ( 𝐴 ∖ { ∅ } )