Theorem dmxrncnvep

Description: Domain of the range product with converse epsilon relation. (Contributed by Peter Mazsa, 23-Nov-2025)

	Ref	Expression
Assertion	dmxrncnvep	⊢ dom ( 𝑅 ⋉ ◡ E ) = ( dom 𝑅 ∖ { ∅ } )

Proof

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