Theorem xpssres

Description: Restriction of a constant function (or other Cartesian product). (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		df-res	|- ( ( A X. B ) |` C ) = ( ( A X. B ) i^i ( C X. _V ) )
2		inxp	|- ( ( A X. B ) i^i ( C X. _V ) ) = ( ( A i^i C ) X. ( B i^i _V ) )
3		inv1	|- ( B i^i _V ) = B
4	3	xpeq2i	|- ( ( A i^i C ) X. ( B i^i _V ) ) = ( ( A i^i C ) X. B )
5	1 2 4	3eqtri	|- ( ( A X. B ) |` C ) = ( ( A i^i C ) X. B )
6		sseqin2	|- ( C C_ A <-> ( A i^i C ) = C )
7	6	biimpi	|- ( C C_ A -> ( A i^i C ) = C )
8	7	xpeq1d	|- ( C C_ A -> ( ( A i^i C ) X. B ) = ( C X. B ) )
9	5 8	syl5eq	|- ( C C_ A -> ( ( A X. B ) |` C ) = ( C X. B ) )