ecinn0

Description: Two ways of saying that the coset of A and the coset of B have some elements in common. (Contributed by Peter Mazsa, 23-Jan-2019)

		Ref	Expression
	Assertion	ecinn0	$⊢ (A \in V \land B \in W) \to ([A] R \cap [B] R \neq \emptyset \leftrightarrow \exists x (A R x \land B R x))$

Step	Hyp	Ref	Expression
1		ecin0	$⊢ (A \in V \land B \in W) \to ([A] R \cap [B] R = \emptyset \leftrightarrow \forall x (A R x \to \neg B R x))$
2	1	necon3abid	$⊢ (A \in V \land B \in W) \to ([A] R \cap [B] R \neq \emptyset \leftrightarrow \neg \forall x (A R x \to \neg B R x))$
3		notnotb	$⊢ B R x \leftrightarrow \neg \neg B R x$
4	3	anbi2i	$⊢ (A R x \land B R x) \leftrightarrow (A R x \land \neg \neg B R x)$
5	4	exbii	$⊢ \exists x (A R x \land B R x) \leftrightarrow \exists x (A R x \land \neg \neg B R x)$
6		exanali	$⊢ \exists x (A R x \land \neg \neg B R x) \leftrightarrow \neg \forall x (A R x \to \neg B R x)$
7	5 6	bitri	$⊢ \exists x (A R x \land B R x) \leftrightarrow \neg \forall x (A R x \to \neg B R x)$
8	2 7	bitr4di	$⊢ (A \in V \land B \in W) \to ([A] R \cap [B] R \neq \emptyset \leftrightarrow \exists x (A R x \land B R x))$

Metamath Proof Explorer