Description: Distributive law for restriction over difference. (Contributed by BTernaryTau, 15-Aug-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | resdifdir | ⊢ ( ( 𝐴 ∖ 𝐵 ) ↾ 𝐶 ) = ( ( 𝐴 ↾ 𝐶 ) ∖ ( 𝐵 ↾ 𝐶 ) ) |
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 | ⊢ ( ( 𝐴 ∖ 𝐵 ) ↾ 𝐶 ) = ( ( 𝐴 ↾ 𝐶 ) ∖ ( 𝐵 ↾ 𝐶 ) ) |