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

Metamath Proof Explorer

Theorem resiun2

Description: Distribution of restriction over indexed union. (Contributed by Mario Carneiro, 29-May-2015)

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

Proof

Step Hyp Ref Expression
1 df-res 
 |-  ( C |` U_ x e. A B ) = ( C i^i ( U_ x e. A B X. _V ) )
2 df-res 
 |-  ( C |` B ) = ( C i^i ( B X. _V ) )
3 2 a1i 
 |-  ( x e. A -> ( C |` B ) = ( C i^i ( B X. _V ) ) )
4 3 iuneq2i 
 |-  U_ x e. A ( C |` B ) = U_ x e. A ( C i^i ( B X. _V ) )
5 xpiundir 
 |-  ( U_ x e. A B X. _V ) = U_ x e. A ( B X. _V )
6 5 ineq2i 
 |-  ( C i^i ( U_ x e. A B X. _V ) ) = ( C i^i U_ x e. A ( B X. _V ) )
7 iunin2 
 |-  U_ x e. A ( C i^i ( B X. _V ) ) = ( C i^i U_ x e. A ( B X. _V ) )
8 6 7 eqtr4i 
 |-  ( C i^i ( U_ x e. A B X. _V ) ) = U_ x e. A ( C i^i ( B X. _V ) )
9 4 8 eqtr4i 
 |-  U_ x e. A ( C |` B ) = ( C i^i ( U_ x e. A B X. _V ) )
10 1 9 eqtr4i 
 |-  ( C |` U_ x e. A B ) = U_ x e. A ( C |` B )