Theorem xpssres

Description: Restriction of a Cartesian product to a subclass of the first factor. (Contributed by Stefan O'Rear, 24-Jan-2015)

	Ref	Expression
Assertion	xpssres	|- ( C C_ A -> ( ( A X. B ) |` C ) = ( C X. B ) )

Proof

Step	Hyp	Ref	Expression
1		xpres	|- ( ( A X. B ) |` C ) = ( ( A i^i C ) X. B )
2		sseqin2	|- ( C C_ A <-> ( A i^i C ) = C )
3	2	biimpi	|- ( C C_ A -> ( A i^i C ) = C )
4	3	xpeq1d	|- ( C C_ A -> ( ( A i^i C ) X. B ) = ( C X. B ) )
5	1 4	eqtrid	|- ( C C_ A -> ( ( A X. B ) |` C ) = ( C X. B ) )