Metamath Proof Explorer

Theorem resiun1

Description: Distribution of restriction over indexed union. (Contributed by Mario Carneiro, 29-May-2015) (Proof shortened by JJ, 25-Aug-2021)

Ref Expression
Assertion resiun1 
|- ( U_ x e. A B |` C ) = U_ x e. A ( B |` C )

Proof

Step Hyp Ref Expression
1 iunin1 
 |-  U_ x e. A ( B i^i ( C X. _V ) ) = ( U_ x e. A B i^i ( C X. _V ) )
2 df-res 
 |-  ( B |` C ) = ( B i^i ( C X. _V ) )
3 2 a1i 
 |-  ( x e. A -> ( B |` C ) = ( B i^i ( C X. _V ) ) )
4 3 iuneq2i 
 |-  U_ x e. A ( B |` C ) = U_ x e. A ( B i^i ( C X. _V ) )
5 df-res 
 |-  ( U_ x e. A B |` C ) = ( U_ x e. A B i^i ( C X. _V ) )
6 1 4 5 3eqtr4ri 
 |-  ( U_ x e. A B |` C ) = U_ x e. A ( B |` C )