Metamath Proof Explorer


Theorem resdifdir

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

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

Proof

Step Hyp Ref Expression
1 indifdir ( ( 𝐴𝐵 ) ∩ ( 𝐶 × V ) ) = ( ( 𝐴 ∩ ( 𝐶 × V ) ) ∖ ( 𝐵 ∩ ( 𝐶 × V ) ) )
2 df-res ( ( 𝐴𝐵 ) ↾ 𝐶 ) = ( ( 𝐴𝐵 ) ∩ ( 𝐶 × V ) )
3 df-res ( 𝐴𝐶 ) = ( 𝐴 ∩ ( 𝐶 × V ) )
4 df-res ( 𝐵𝐶 ) = ( 𝐵 ∩ ( 𝐶 × V ) )
5 3 4 difeq12i ( ( 𝐴𝐶 ) ∖ ( 𝐵𝐶 ) ) = ( ( 𝐴 ∩ ( 𝐶 × V ) ) ∖ ( 𝐵 ∩ ( 𝐶 × V ) ) )
6 1 2 5 3eqtr4i ( ( 𝐴𝐵 ) ↾ 𝐶 ) = ( ( 𝐴𝐶 ) ∖ ( 𝐵𝐶 ) )