Theorem dmuncnvepres

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

	Ref	Expression
Assertion	dmuncnvepres	|- dom ( ( R u. `' _E ) |` A ) = ( A i^i ( dom R u. ( _V \ { (/) } ) ) )

Proof

Step	Hyp	Ref	Expression
1		dmres	|- dom ( ( R u. `' _E ) |` A ) = ( A i^i dom ( R u. `' _E ) )
2		dmun	|- dom ( R u. `' _E ) = ( dom R u. dom `' _E )
3		dmcnvep	|- dom `' _E = ( _V \ { (/) } )
4	3	uneq2i	|- ( dom R u. dom `' _E ) = ( dom R u. ( _V \ { (/) } ) )
5	2 4	eqtri	|- dom ( R u. `' _E ) = ( dom R u. ( _V \ { (/) } ) )
6	5	ineq2i	|- ( A i^i dom ( R u. `' _E ) ) = ( A i^i ( dom R u. ( _V \ { (/) } ) ) )
7	1 6	eqtri	|- dom ( ( R u. `' _E ) |` A ) = ( A i^i ( dom R u. ( _V \ { (/) } ) ) )