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	⊢ ( 𝐶 ⊆ 𝐴 → ( ( 𝐴 × 𝐵 ) ↾ 𝐶 ) = ( 𝐶 × 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		xpres	⊢ ( ( 𝐴 × 𝐵 ) ↾ 𝐶 ) = ( ( 𝐴 ∩ 𝐶 ) × 𝐵 )
2		sseqin2	⊢ ( 𝐶 ⊆ 𝐴 ↔ ( 𝐴 ∩ 𝐶 ) = 𝐶 )
3	2	biimpi	⊢ ( 𝐶 ⊆ 𝐴 → ( 𝐴 ∩ 𝐶 ) = 𝐶 )
4	3	xpeq1d	⊢ ( 𝐶 ⊆ 𝐴 → ( ( 𝐴 ∩ 𝐶 ) × 𝐵 ) = ( 𝐶 × 𝐵 ) )
5	1 4	eqtrid	⊢ ( 𝐶 ⊆ 𝐴 → ( ( 𝐴 × 𝐵 ) ↾ 𝐶 ) = ( 𝐶 × 𝐵 ) )