Theorem ecuncnvepres

Description: The restricted union with converse epsilon relation coset of B . (Contributed by Peter Mazsa, 28-Jan-2026)

	Ref	Expression
Assertion	ecuncnvepres	|- ( B e. A -> [ B ] ( ( R u. `' _E ) |` A ) = ( B u. [ B ] R ) )

Proof

Step	Hyp	Ref	Expression
1		ecunres	|- ( B e. A -> [ B ] ( ( R u. `' _E ) |` A ) = ( [ B ] ( R |` A ) u. [ B ] ( `' _E |` A ) ) )
2		elecreseq	|- ( B e. A -> [ B ] ( R |` A ) = [ B ] R )
3		eccnvepres2	|- ( B e. A -> [ B ] ( `' _E |` A ) = B )
4	2 3	uneq12d	|- ( B e. A -> ( [ B ] ( R |` A ) u. [ B ] ( `' _E |` A ) ) = ( [ B ] R u. B ) )
5	1 4	eqtrd	|- ( B e. A -> [ B ] ( ( R u. `' _E ) |` A ) = ( [ B ] R u. B ) )
6		uncom	|- ( [ B ] R u. B ) = ( B u. [ B ] R )
7	5 6	eqtrdi	|- ( B e. A -> [ B ] ( ( R u. `' _E ) |` A ) = ( B u. [ B ] R ) )