Metamath Proof Explorer

Theorem resdifdi

Description: Distributive law for restriction over difference. (Contributed by BTernaryTau, 15-Aug-2024)

Ref Expression
Assertion resdifdi ( 𝐴 ↾ ( 𝐵 ∖ 𝐶 ) ) = ( ( 𝐴 ↾ 𝐵 ) ∖ ( 𝐴 ↾ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 df-res ⊢ ( 𝐴 ↾ ( 𝐵 ∖ 𝐶 ) ) = ( 𝐴 ∩ ( ( 𝐵 ∖ 𝐶 ) × V ) )
2 difxp1 ⊢ ( ( 𝐵 ∖ 𝐶 ) × V ) = ( ( 𝐵 × V ) ∖ ( 𝐶 × V ) )
3 2 ineq2i ⊢ ( 𝐴 ∩ ( ( 𝐵 ∖ 𝐶 ) × V ) ) = ( 𝐴 ∩ ( ( 𝐵 × V ) ∖ ( 𝐶 × V ) ) )
4 indifdi ⊢ ( 𝐴 ∩ ( ( 𝐵 × V ) ∖ ( 𝐶 × V ) ) ) = ( ( 𝐴 ∩ ( 𝐵 × V ) ) ∖ ( 𝐴 ∩ ( 𝐶 × V ) ) )
5 1 3 4 3eqtri ⊢ ( 𝐴 ↾ ( 𝐵 ∖ 𝐶 ) ) = ( ( 𝐴 ∩ ( 𝐵 × V ) ) ∖ ( 𝐴 ∩ ( 𝐶 × V ) ) )
6 df-res ⊢ ( 𝐴 ↾ 𝐵 ) = ( 𝐴 ∩ ( 𝐵 × V ) )
7 df-res ⊢ ( 𝐴 ↾ 𝐶 ) = ( 𝐴 ∩ ( 𝐶 × V ) )
8 6 7 difeq12i ⊢ ( ( 𝐴 ↾ 𝐵 ) ∖ ( 𝐴 ↾ 𝐶 ) ) = ( ( 𝐴 ∩ ( 𝐵 × V ) ) ∖ ( 𝐴 ∩ ( 𝐶 × V ) ) )
9 5 8 eqtr4i ⊢ ( 𝐴 ↾ ( 𝐵 ∖ 𝐶 ) ) = ( ( 𝐴 ↾ 𝐵 ) ∖ ( 𝐴 ↾ 𝐶 ) )