Metamath Proof Explorer


Theorem resindi

Description: Class restriction distributes over intersection. (Contributed by FL, 6-Oct-2008)

Ref Expression
Assertion resindi ABC=ABAC

Proof

Step Hyp Ref Expression
1 xpindir BC×V=B×VC×V
2 1 ineq2i ABC×V=AB×VC×V
3 inindi AB×VC×V=AB×VAC×V
4 2 3 eqtri ABC×V=AB×VAC×V
5 df-res ABC=ABC×V
6 df-res AB=AB×V
7 df-res AC=AC×V
8 6 7 ineq12i ABAC=AB×VAC×V
9 4 5 8 3eqtr4i ABC=ABAC