This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )