Metamath Proof Explorer

Theorem inelcm

Description: The intersection of classes with a common member is nonempty. (Contributed by NM, 7-Apr-1994)

		Ref	Expression
	Assertion	inelcm	$⊢ (A \in B \land A \in C) \to B \cap C \neq \emptyset$

Step	Hyp	Ref	Expression
1		elin	$⊢ A \in (B \cap C) \leftrightarrow (A \in B \land A \in C)$
2		ne0i	$⊢ A \in (B \cap C) \to B \cap C \neq \emptyset$
3	1 2	sylbir	$⊢ (A \in B \land A \in C) \to B \cap C \neq \emptyset$