Metamath Proof Explorer

Theorem elriin

Description: Elementhood in a relative intersection. (Contributed by Mario Carneiro, 30-Dec-2016)

		Ref	Expression
	Assertion	elriin	$⊢ B \in (A \cap ⋂_{x \in X} S) \leftrightarrow (B \in A \land \forall x \in X B \in S)$

Step	Hyp	Ref	Expression
1		elin	$⊢ B \in (A \cap ⋂_{x \in X} S) \leftrightarrow (B \in A \land B \in ⋂_{x \in X} S)$
2		eliin	$⊢ B \in A \to (B \in ⋂_{x \in X} S \leftrightarrow \forall x \in X B \in S)$
3	2	pm5.32i	$⊢ (B \in A \land B \in ⋂_{x \in X} S) \leftrightarrow (B \in A \land \forall x \in X B \in S)$
4	1 3	bitri	$⊢ B \in (A \cap ⋂_{x \in X} S) \leftrightarrow (B \in A \land \forall x \in X B \in S)$