Theorem elrint2

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

	Ref	Expression
Assertion	elrint2	$$⊢X\in A\to \left(X\in \left(A\cap \bigcap B\right)\leftrightarrow \forall y\in BX\in y\right)$$

Proof

Step	Hyp	Ref	Expression
1		elrint	$$⊢X\in \left(A\cap \bigcap B\right)\leftrightarrow \left(X\in A\wedge \forall y\in BX\in y\right)$$
2	1	baib	$$⊢X\in A\to \left(X\in \left(A\cap \bigcap B\right)\leftrightarrow \forall y\in BX\in y\right)$$