Theorem inres2

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

	Ref	Expression
Assertion	inres2	|- ( ( R |` A ) i^i S ) = ( ( R i^i S ) |` A )

Proof

Step	Hyp	Ref	Expression
1		inres	|- ( S i^i ( R |` A ) ) = ( ( S i^i R ) |` A )
2	1	ineqcomi	|- ( ( R |` A ) i^i S ) = ( ( S i^i R ) |` A )
3		incom	|- ( R i^i S ) = ( S i^i R )
4	3	reseq1i	|- ( ( R i^i S ) |` A ) = ( ( S i^i R ) |` A )
5	2 4	eqtr4i	|- ( ( R |` A ) i^i S ) = ( ( R i^i S ) |` A )