Metamath Proof Explorer

Theorem ssin

Description: Subclass of intersection. Theorem 2.8(vii) of Monk1 p. 26. (Contributed by NM, 15-Jun-2004) (Proof shortened by Andrew Salmon, 26-Jun-2011)

		Ref	Expression
	Assertion	ssin	$⊢ (A \subseteq B \land A \subseteq C) \leftrightarrow A \subseteq B \cap C$

Proof

Step	Hyp	Ref	Expression
1		elin	$⊢ x \in (B \cap C) \leftrightarrow (x \in B \land x \in C)$
2	1	imbi2i	$⊢ (x \in A \to x \in (B \cap C)) \leftrightarrow (x \in A \to (x \in B \land x \in C))$
3	2	albii	$⊢ \forall x (x \in A \to x \in (B \cap C)) \leftrightarrow \forall x (x \in A \to (x \in B \land x \in C))$
4		jcab	$⊢ (x \in A \to (x \in B \land x \in C)) \leftrightarrow ((x \in A \to x \in B) \land (x \in A \to x \in C))$
5	4	albii	$⊢ \forall x (x \in A \to (x \in B \land x \in C)) \leftrightarrow \forall x ((x \in A \to x \in B) \land (x \in A \to x \in C))$
6		19.26	$⊢ \forall x ((x \in A \to x \in B) \land (x \in A \to x \in C)) \leftrightarrow (\forall x (x \in A \to x \in B) \land \forall x (x \in A \to x \in C))$
7	3 5 6	3bitrri	$⊢ (\forall x (x \in A \to x \in B) \land \forall x (x \in A \to x \in C)) \leftrightarrow \forall x (x \in A \to x \in (B \cap C))$
8		df-ss	$⊢ A \subseteq B \leftrightarrow \forall x (x \in A \to x \in B)$
9		df-ss	$⊢ A \subseteq C \leftrightarrow \forall x (x \in A \to x \in C)$
10	8 9	anbi12i	$⊢ (A \subseteq B \land A \subseteq C) \leftrightarrow (\forall x (x \in A \to x \in B) \land \forall x (x \in A \to x \in C))$
11		df-ss	$⊢ A \subseteq B \cap C \leftrightarrow \forall x (x \in A \to x \in (B \cap C))$
12	7 10 11	3bitr4i	$⊢ (A \subseteq B \land A \subseteq C) \leftrightarrow A \subseteq B \cap C$