Theorem resindi

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

	Ref	Expression
Assertion	resindi	|- ( A |` ( B i^i C ) ) = ( ( A |` B ) i^i ( A |` C ) )

Proof

Step	Hyp	Ref	Expression
1		xpindir	|- ( ( B i^i C ) X. _V ) = ( ( B X. _V ) i^i ( C X. _V ) )
2	1	ineq2i	|- ( A i^i ( ( B i^i C ) X. _V ) ) = ( A i^i ( ( B X. _V ) i^i ( C X. _V ) ) )
3		inindi	|- ( A i^i ( ( B X. _V ) i^i ( C X. _V ) ) ) = ( ( A i^i ( B X. _V ) ) i^i ( A i^i ( C X. _V ) ) )
4	2 3	eqtri	|- ( A i^i ( ( B i^i C ) X. _V ) ) = ( ( A i^i ( B X. _V ) ) i^i ( A i^i ( C X. _V ) ) )
5		df-res	|- ( A |` ( B i^i C ) ) = ( A i^i ( ( B i^i C ) X. _V ) )
6		df-res	|- ( A |` B ) = ( A i^i ( B X. _V ) )
7		df-res	|- ( A |` C ) = ( A i^i ( C X. _V ) )
8	6 7	ineq12i	|- ( ( A |` B ) i^i ( A |` C ) ) = ( ( A i^i ( B X. _V ) ) i^i ( A i^i ( C X. _V ) ) )
9	4 5 8	3eqtr4i	|- ( A |` ( B i^i C ) ) = ( ( A |` B ) i^i ( A |` C ) )