Metamath Proof Explorer

Theorem ssrin

Description: Add right intersection to subclass relation. (Contributed by NM, 16-Aug-1994) (Proof shortened by Andrew Salmon, 26-Jun-2011)

		Ref	Expression
	Assertion	ssrin	$⊢ A \subseteq B \to A \cap C \subseteq B \cap C$

Step	Hyp	Ref	Expression
1		ssel	$⊢ A \subseteq B \to (x \in A \to x \in B)$
2	1	anim1d	$⊢ A \subseteq B \to ((x \in A \land x \in C) \to (x \in B \land x \in C))$
3		elin	$⊢ x \in (A \cap C) \leftrightarrow (x \in A \land x \in C)$
4		elin	$⊢ x \in (B \cap C) \leftrightarrow (x \in B \land x \in C)$
5	2 3 4	3imtr4g	$⊢ A \subseteq B \to (x \in (A \cap C) \to x \in (B \cap C))$
6	5	ssrdv	$⊢ A \subseteq B \to A \cap C \subseteq B \cap C$