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

Metamath Proof Explorer

Theorem ecun

Description: The union coset of A . (Contributed by Peter Mazsa, 28-Jan-2026)

Ref Expression
Assertion ecun 
|- ( A e. V -> [ A ] ( R u. S ) = ( [ A ] R u. [ A ] S ) )

Proof

Step Hyp Ref Expression
1 unab 
 |-  ( { x | A R x } u. { x | A S x } ) = { x | ( A R x \/ A S x ) }
2 1 a1i 
 |-  ( A e. V -> ( { x | A R x } u. { x | A S x } ) = { x | ( A R x \/ A S x ) } )
3 dfec2 
 |-  ( A e. V -> [ A ] R = { x | A R x } )
4 dfec2 
 |-  ( A e. V -> [ A ] S = { x | A S x } )
5 3 4 uneq12d 
 |-  ( A e. V -> ( [ A ] R u. [ A ] S ) = ( { x | A R x } u. { x | A S x } ) )
6 elecALTV 
 |-  ( ( A e. V /\ x e. _V ) -> ( x e. [ A ] ( R u. S ) <-> A ( R u. S ) x ) )
7 6 elvd 
 |-  ( A e. V -> ( x e. [ A ] ( R u. S ) <-> A ( R u. S ) x ) )
8 brun 
 |-  ( A ( R u. S ) x <-> ( A R x \/ A S x ) )
9 7 8 bitrdi 
 |-  ( A e. V -> ( x e. [ A ] ( R u. S ) <-> ( A R x \/ A S x ) ) )
10 9 eqabdv 
 |-  ( A e. V -> [ A ] ( R u. S ) = { x | ( A R x \/ A S x ) } )
11 2 5 10 3eqtr4rd 
 |-  ( A e. V -> [ A ] ( R u. S ) = ( [ A ] R u. [ A ] S ) )