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 )