Theorem elin2

Description: Membership in a class defined as an intersection. (Contributed by Stefan O'Rear, 29-Mar-2015)

	Ref	Expression
Hypothesis	elin2.x	$$⊢X=B\cap C$$
Assertion	elin2	$$⊢A\in X\leftrightarrow \left(A\in B\wedge A\in C\right)$$

Proof

Step	Hyp	Ref	Expression
1		elin2.x	$$⊢X=B\cap C$$
2	1	eleq2i	$$⊢A\in X\leftrightarrow A\in \left(B\cap C\right)$$
3		elin	$$⊢A\in \left(B\cap C\right)\leftrightarrow \left(A\in B\wedge A\in C\right)$$
4	2 3	bitri	$$⊢A\in X\leftrightarrow \left(A\in B\wedge A\in C\right)$$