Theorem dmxrncnvepres

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

	Ref	Expression
Assertion	dmxrncnvepres	|- dom ( R |X. ( `' _E |` A ) ) = ( dom ( R |` A ) \ { (/) } )

Proof

Step	Hyp	Ref	Expression
1		xrnres	|- ( ( R |X. `' _E ) |` A ) = ( ( R |` A ) |X. `' _E )
2		xrnres2	|- ( ( R |X. `' _E ) |` A ) = ( R |X. ( `' _E |` A ) )
3	1 2	eqtr3i	|- ( ( R |` A ) |X. `' _E ) = ( R |X. ( `' _E |` A ) )
4	3	dmeqi	|- dom ( ( R |` A ) |X. `' _E ) = dom ( R |X. ( `' _E |` A ) )
5		dmxrncnvep	|- dom ( ( R |` A ) |X. `' _E ) = ( dom ( R |` A ) \ { (/) } )
6	4 5	eqtr3i	|- dom ( R |X. ( `' _E |` A ) ) = ( dom ( R |` A ) \ { (/) } )