inxpssres

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

		Ref	Expression
	Assertion	inxpssres	$⊢ R \cap (A \times B) \subseteq {R ↾}_{A}$

Step	Hyp	Ref	Expression
1		ssid	$⊢ A \subseteq A$
2		ssv	$⊢ B \subseteq V$
3		xpss12	$⊢ (A \subseteq A \land B \subseteq V) \to A \times B \subseteq A \times V$
4	1 2 3	mp2an	$⊢ A \times B \subseteq A \times V$
5		sslin	$⊢ A \times B \subseteq A \times V \to R \cap (A \times B) \subseteq R \cap (A \times V)$
6	4 5	ax-mp	$⊢ R \cap (A \times B) \subseteq R \cap (A \times V)$
7		df-res	$⊢ {R ↾}_{A} = R \cap (A \times V)$
8	6 7	sseqtrri	$⊢ R \cap (A \times B) \subseteq {R ↾}_{A}$

Metamath Proof Explorer