inn0f

Description: A nonempty intersection. (Contributed by Glauco Siliprandi, 24-Dec-2020)

	Ref	Expression
Hypotheses	inn0f.1	$⊢ \underline{Ⅎ} x A$
	inn0f.2	$⊢ \underline{Ⅎ} x B$
Assertion	inn0f	$⊢ A \cap B \neq \emptyset \leftrightarrow \exists x \in A x \in B$

Step	Hyp	Ref	Expression
1		inn0f.1	$⊢ \underline{Ⅎ} x A$
2		inn0f.2	$⊢ \underline{Ⅎ} x B$
3		elin	$⊢ x \in (A \cap B) \leftrightarrow (x \in A \land x \in B)$
4	3	exbii	$⊢ \exists x x \in (A \cap B) \leftrightarrow \exists x (x \in A \land x \in B)$
5	1 2	nfin	$⊢ \underline{Ⅎ} x (A \cap B)$
6	5	n0f	$⊢ A \cap B \neq \emptyset \leftrightarrow \exists x x \in (A \cap B)$
7		df-rex	$⊢ \exists x \in A x \in B \leftrightarrow \exists x (x \in A \land x \in B)$
8	4 6 7	3bitr4i	$⊢ A \cap B \neq \emptyset \leftrightarrow \exists x \in A x \in B$

Metamath Proof Explorer