Theorem inres

Description: Move intersection into class restriction. (Contributed by NM, 18-Dec-2008)

	Ref	Expression
Assertion	inres	$$⊢A\cap \left({B\upharpoonright }_C\right)={\left(A\cap B\right)\upharpoonright }_C$$

Proof

Step	Hyp	Ref	Expression
1		inass	$$⊢\left(A\cap B\right)\cap \left(C\times \mathrm{V}\right)=A\cap \left(B\cap \left(C\times \mathrm{V}\right)\right)$$
2		df-res	$$⊢{\left(A\cap B\right)\upharpoonright }_C=\left(A\cap B\right)\cap \left(C\times \mathrm{V}\right)$$
3		df-res	$$⊢{B\upharpoonright }_C=B\cap \left(C\times \mathrm{V}\right)$$
4	3	ineq2i	$$⊢A\cap \left({B\upharpoonright }_C\right)=A\cap \left(B\cap \left(C\times \mathrm{V}\right)\right)$$
5	1 2 4	3eqtr4ri	$$⊢A\cap \left({B\upharpoonright }_C\right)={\left(A\cap B\right)\upharpoonright }_C$$