Theorem elinel1

Description: Membership in an intersection implies membership in the first set. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Assertion	elinel1	$$⊢A\in \left(B\cap C\right)\to A\in B$$

Proof

Step	Hyp	Ref	Expression
1		elin	$$⊢A\in \left(B\cap C\right)\leftrightarrow \left(A\in B\wedge A\in C\right)$$
2	1	simplbi	$$⊢A\in \left(B\cap C\right)\to A\in B$$