Theorem inxpssres

Description: Intersection with a Cartesian product is a subclass of restriction. (Contributed by Peter Mazsa, 19-Jul-2019)

	Ref	Expression
Assertion	inxpssres	⊢ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ⊆ ( 𝑅 ↾ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		ssid	⊢ 𝐴 ⊆ 𝐴
2		ssv	⊢ 𝐵 ⊆ V
3		xpss12	⊢ ( ( 𝐴 ⊆ 𝐴 ∧ 𝐵 ⊆ V ) → ( 𝐴 × 𝐵 ) ⊆ ( 𝐴 × V ) )
4	1 2 3	mp2an	⊢ ( 𝐴 × 𝐵 ) ⊆ ( 𝐴 × V )
5		sslin	⊢ ( ( 𝐴 × 𝐵 ) ⊆ ( 𝐴 × V ) → ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ⊆ ( 𝑅 ∩ ( 𝐴 × V ) ) )
6	4 5	ax-mp	⊢ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ⊆ ( 𝑅 ∩ ( 𝐴 × V ) )
7		df-res	⊢ ( 𝑅 ↾ 𝐴 ) = ( 𝑅 ∩ ( 𝐴 × V ) )
8	6 7	sseqtrri	⊢ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ⊆ ( 𝑅 ↾ 𝐴 )