Metamath Proof Explorer

Theorem resiun2

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

Ref Expression
Assertion resiun2 ( 𝐶 ↾ ∪ 𝑥 ∈ 𝐴 𝐵 ) = ∪ 𝑥 ∈ 𝐴 ( 𝐶 ↾ 𝐵 )

Proof

Step Hyp Ref Expression
1 df-res ⊢ ( 𝐶 ↾ ∪ 𝑥 ∈ 𝐴 𝐵 ) = ( 𝐶 ∩ ( ∪ 𝑥 ∈ 𝐴 𝐵 × V ) )
2 df-res ⊢ ( 𝐶 ↾ 𝐵 ) = ( 𝐶 ∩ ( 𝐵 × V ) )
3 2 a1i ⊢ ( 𝑥 ∈ 𝐴 → ( 𝐶 ↾ 𝐵 ) = ( 𝐶 ∩ ( 𝐵 × V ) ) )
4 3 iuneq2i ⊢ ∪ 𝑥 ∈ 𝐴 ( 𝐶 ↾ 𝐵 ) = ∪ 𝑥 ∈ 𝐴 ( 𝐶 ∩ ( 𝐵 × V ) )
5 xpiundir ⊢ ( ∪ 𝑥 ∈ 𝐴 𝐵 × V ) = ∪ 𝑥 ∈ 𝐴 ( 𝐵 × V )
6 5 ineq2i ⊢ ( 𝐶 ∩ ( ∪ 𝑥 ∈ 𝐴 𝐵 × V ) ) = ( 𝐶 ∩ ∪ 𝑥 ∈ 𝐴 ( 𝐵 × V ) )
7 iunin2 ⊢ ∪ 𝑥 ∈ 𝐴 ( 𝐶 ∩ ( 𝐵 × V ) ) = ( 𝐶 ∩ ∪ 𝑥 ∈ 𝐴 ( 𝐵 × V ) )
8 6 7 eqtr4i ⊢ ( 𝐶 ∩ ( ∪ 𝑥 ∈ 𝐴 𝐵 × V ) ) = ∪ 𝑥 ∈ 𝐴 ( 𝐶 ∩ ( 𝐵 × V ) )
9 4 8 eqtr4i ⊢ ∪ 𝑥 ∈ 𝐴 ( 𝐶 ↾ 𝐵 ) = ( 𝐶 ∩ ( ∪ 𝑥 ∈ 𝐴 𝐵 × V ) )
10 1 9 eqtr4i ⊢ ( 𝐶 ↾ ∪ 𝑥 ∈ 𝐴 𝐵 ) = ∪ 𝑥 ∈ 𝐴 ( 𝐶 ↾ 𝐵 )