Metamath Proof Explorer


Theorem resdifdi

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

Ref Expression
Assertion resdifdi A B C = A B A C

Proof

Step Hyp Ref Expression
1 df-res A B C = A B C × V
2 difxp1 B C × V = B × V C × V
3 2 ineq2i A B C × V = A B × V C × V
4 indifdi A B × V C × V = A B × V A C × V
5 1 3 4 3eqtri A B C = A B × V A C × V
6 df-res A B = A B × V
7 df-res A C = A C × V
8 6 7 difeq12i A B A C = A B × V A C × V
9 5 8 eqtr4i A B C = A B A C