Metamath Proof Explorer

Theorem elinsn

Description: If the intersection of two classes is a (proper) singleton, then the singleton element is a member of both classes. (Contributed by AV, 30-Dec-2021)

		Ref	Expression
	Assertion	elinsn	$⊢ (A \in V \land B \cap C = \{A\}) \to (A \in B \land A \in C)$

Proof

Step	Hyp	Ref	Expression
1		snidg	$⊢ A \in V \to A \in \{A\}$
2		eleq2	$⊢ B \cap C = \{A\} \to (A \in (B \cap C) \leftrightarrow A \in \{A\})$
3		elin	$⊢ A \in (B \cap C) \leftrightarrow (A \in B \land A \in C)$
4	3	biimpi	$⊢ A \in (B \cap C) \to (A \in B \land A \in C)$
5	2 4	biimtrrdi	$⊢ B \cap C = \{A\} \to (A \in \{A\} \to (A \in B \land A \in C))$
6	1 5	mpan9	$⊢ (A \in V \land B \cap C = \{A\}) \to (A \in B \land A \in C)$