Theorem resiun2 4775

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

Assertion

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

Distinct variable group:   x, C

Allowed substitution hints:   A( x)   B( x)

Proof of Theorem resiun2

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

Syntax hints:   = wceq 1299   e. wcel 1448   _Vcvv 2641   i^i cin 3020   U_ciun 3760   X. cxp 4475   |` cres 4479

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 671  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-10 1451  ax-11 1452  ax-i12 1453  ax-bndl 1454  ax-4 1455  ax-14 1460  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082  ax-sep 3986  ax-pow 4038  ax-pr 4069

This theorem depends on definitions:  df-bi 116  df-3an 932  df-tru 1302  df-nf 1405  df-sb 1704  df-clab 2087  df-cleq 2093  df-clel 2096  df-nfc 2229  df-ral 2380  df-rex 2381  df-v 2643  df-un 3025  df-in 3027  df-ss 3034  df-pw 3459  df-sn 3480  df-pr 3481  df-op 3483  df-iun 3762  df-opab 3930  df-xp 4483  df-res 4489

This theorem is referenced by: (None)