This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ndisj

Description: Express that an intersection is not empty. (Contributed by RP, 16-Apr-2020)

		Ref	Expression
	Assertion	ndisj	$⊢ A \cap B \neq \emptyset \leftrightarrow \exists x (x \in A \land x \in B)$

Step	Hyp	Ref	Expression
1		n0	$⊢ A \cap B \neq \emptyset \leftrightarrow \exists x x \in (A \cap B)$
2		elin	$⊢ x \in (A \cap B) \leftrightarrow (x \in A \land x \in B)$
3	2	exbii	$⊢ \exists x x \in (A \cap B) \leftrightarrow \exists x (x \in A \land x \in B)$
4	1 3	bitri	$⊢ A \cap B \neq \emptyset \leftrightarrow \exists x (x \in A \land x \in B)$