Theorem inres2

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

	Ref	Expression
Assertion	inres2	⊢ ( ( 𝑅 ↾ 𝐴 ) ∩ 𝑆 ) = ( ( 𝑅 ∩ 𝑆 ) ↾ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		inres	⊢ ( 𝑆 ∩ ( 𝑅 ↾ 𝐴 ) ) = ( ( 𝑆 ∩ 𝑅 ) ↾ 𝐴 )
2	1	ineqcomi	⊢ ( ( 𝑅 ↾ 𝐴 ) ∩ 𝑆 ) = ( ( 𝑆 ∩ 𝑅 ) ↾ 𝐴 )
3		incom	⊢ ( 𝑅 ∩ 𝑆 ) = ( 𝑆 ∩ 𝑅 )
4	3	reseq1i	⊢ ( ( 𝑅 ∩ 𝑆 ) ↾ 𝐴 ) = ( ( 𝑆 ∩ 𝑅 ) ↾ 𝐴 )
5	2 4	eqtr4i	⊢ ( ( 𝑅 ↾ 𝐴 ) ∩ 𝑆 ) = ( ( 𝑅 ∩ 𝑆 ) ↾ 𝐴 )