Theorem inres2

Description: Two ways of expressing the restriction of an intersection. (Contributed by Peter Mazsa, 5-Jun-2021)

	Ref	Expression
Assertion	inres2	$$⊢\left({R\upharpoonright }_A\right)\cap S={\left(R\cap S\right)\upharpoonright }_A$$

Proof

Step	Hyp	Ref	Expression
1		inres	$$⊢S\cap \left({R\upharpoonright }_A\right)={\left(S\cap R\right)\upharpoonright }_A$$
2	1	ineqcomi	$$⊢\left({R\upharpoonright }_A\right)\cap S={\left(S\cap R\right)\upharpoonright }_A$$
3		incom	$$⊢R\cap S=S\cap R$$
4	3	reseq1i	$$⊢{\left(R\cap S\right)\upharpoonright }_A={\left(S\cap R\right)\upharpoonright }_A$$
5	2 4	eqtr4i	$$⊢\left({R\upharpoonright }_A\right)\cap S={\left(R\cap S\right)\upharpoonright }_A$$