Metamath Proof Explorer

Theorem elrint

Description: Membership in a restricted intersection. (Contributed by Stefan O'Rear, 3-Apr-2015)

		Ref	Expression
	Assertion	elrint	$⊢ X \in (A \cap ⋂ B) \leftrightarrow (X \in A \land \forall y \in B X \in y)$

Step	Hyp	Ref	Expression
1		elin	$⊢ X \in (A \cap ⋂ B) \leftrightarrow (X \in A \land X \in ⋂ B)$
2		elintg	$⊢ X \in A \to (X \in ⋂ B \leftrightarrow \forall y \in B X \in y)$
3	2	pm5.32i	$⊢ (X \in A \land X \in ⋂ B) \leftrightarrow (X \in A \land \forall y \in B X \in y)$
4	1 3	bitri	$⊢ X \in (A \cap ⋂ B) \leftrightarrow (X \in A \land \forall y \in B X \in y)$