Theorem dmxrnuncnvepres

Description: Domain of the range Cartesian product with the converse epsilon relation combined with the union with the converse epsilon, restricted. (Contributed by Peter Mazsa, 28-Jan-2026)

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

Proof

Step	Hyp	Ref	Expression
1		dmuncnvepres	|- dom ( ( ( R |X. `' _E ) u. `' _E ) |` A ) = ( A i^i ( dom ( R |X. `' _E ) u. ( _V \ { (/) } ) ) )
2		dmxrncnvep	|- dom ( R |X. `' _E ) = ( dom R \ { (/) } )
3	2	uneq1i	|- ( dom ( R |X. `' _E ) u. ( _V \ { (/) } ) ) = ( ( dom R \ { (/) } ) u. ( _V \ { (/) } ) )
4		difundir	|- ( ( dom R u. _V ) \ { (/) } ) = ( ( dom R \ { (/) } ) u. ( _V \ { (/) } ) )
5		unv	|- ( dom R u. _V ) = _V
6	5	difeq1i	|- ( ( dom R u. _V ) \ { (/) } ) = ( _V \ { (/) } )
7	3 4 6	3eqtr2i	|- ( dom ( R |X. `' _E ) u. ( _V \ { (/) } ) ) = ( _V \ { (/) } )
8	7	ineq2i	|- ( A i^i ( dom ( R |X. `' _E ) u. ( _V \ { (/) } ) ) ) = ( A i^i ( _V \ { (/) } ) )
9		invdif	|- ( A i^i ( _V \ { (/) } ) ) = ( A \ { (/) } )
10	1 8 9	3eqtri	|- dom ( ( ( R |X. `' _E ) u. `' _E ) |` A ) = ( A \ { (/) } )